Skip to content

Commit 2da9845

Browse files
committed
resolve PR comments
1 parent 09b4c16 commit 2da9845

File tree

4 files changed

+19
-4
lines changed

4 files changed

+19
-4
lines changed

src/haz3lcore/derived/Measured.re

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -325,7 +325,6 @@ let of_segment =
325325
~col=new_indent - origin.col,
326326
);
327327
// add seg to map and reset seg
328-
//TODO(andrew): decide if should actually add linebreak here
329328
let map =
330329
add_piece_row(
331330
origin.row,

src/haz3lcore/lang/Token.re

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ let bounding_box = (t: t): Point.t =>
4242
/* Token Recognition Predicates */
4343

4444
/* A. Secondary Notation (Comments, Whitespace, etc.) */
45-
let empty = "";
45+
let empty = ""; /* This is invalid for view */
4646
let space = " ";
4747
let linebreak = "\n";
4848
let comment_regexp = regexp("^#[^#\n]*#$"); /* Multiline comments not supported */

src/web/view/NutMenu.re

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,21 @@ let dev_group = (~globals: Globals.t) => {
116116
Benchmark: Settings.Update.t,
117117
),
118118
("𝑒", "Elaboration", globals.settings.core.elaborate, Elaborate),
119-
("↵", "Whitespace", globals.settings.secondary_icons, SecondaryIcons),
119+
],
120+
);
121+
};
122+
123+
let code_display_group = (~globals: Globals.t) => {
124+
settings_group(
125+
~globals,
126+
"Code Display",
127+
[
128+
(
129+
"↵",
130+
"Whitespace",
131+
globals.settings.secondary_icons,
132+
SecondaryIcons: Settings.Update.t,
133+
),
120134
(
121135
"a",
122136
"Animations",
@@ -139,12 +153,14 @@ let dev_group = (~globals: Globals.t) => {
139153
),
140154
);
141155
};
156+
142157
//("l", "Line Numbers", globals.settings.line_numbers, ToggleLineNumbers)
143158
let settings_menu = (~globals) => {
144159
[
145160
semantics_group(~globals),
146161
values_group(~globals),
147162
stepper_group(~globals),
148163
dev_group(~globals),
164+
code_display_group(~globals),
149165
];
150166
};

src/web/www/style/editor.css

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,7 @@
6767
* to avoid inserting an extraneous whitespace context for inline
6868
* syntax views, e.g. type views in the cursor inspector */
6969
.code-text:after {
70-
content: "";
70+
content: "";
7171
}
7272

7373

0 commit comments

Comments
 (0)