--- a/src/Pure/General/antiquote.ML Fri Jan 19 11:25:55 2018 +0100
+++ b/src/Pure/General/antiquote.ML Fri Jan 19 11:26:31 2018 +0100
@@ -10,7 +10,8 @@
type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
type text_antiquote = Symbol_Pos.T list antiquote
- val range: text_antiquote list -> Position.range
+ val text_antiquote_range: text_antiquote -> Position.range
+ val text_range: text_antiquote list -> Position.range
val split_lines: text_antiquote list -> text_antiquote list list
val antiq_reports: 'a antiquote list -> Position.report list
val scan_control: control scanner
@@ -31,13 +32,14 @@
type text_antiquote = Symbol_Pos.T list antiquote;
-fun antiquote_range (Text ss) = Symbol_Pos.range ss
- | antiquote_range (Control {range, ...}) = range
- | antiquote_range (Antiq {range, ...}) = range;
+fun text_antiquote_range (Text ss) = Symbol_Pos.range ss
+ | text_antiquote_range (Control {range, ...}) = range
+ | text_antiquote_range (Antiq {range, ...}) = range;
-fun range ants =
+fun text_range ants =
if null ants then Position.no_range
- else Position.range (#1 (antiquote_range (hd ants)), #2 (antiquote_range (List.last ants)));
+ else
+ Position.range (#1 (text_antiquote_range (hd ants)), #2 (text_antiquote_range (List.last ants)));
(* split lines *)
--- a/src/Pure/Thy/markdown.ML Fri Jan 19 11:25:55 2018 +0100
+++ b/src/Pure/Thy/markdown.ML Fri Jan 19 11:26:31 2018 +0100
@@ -132,8 +132,8 @@
fun block_source (Par lines) = maps line_source lines
| block_source (List {body, ...}) = maps line_source (maps block_lines body);
-fun block_range (Par lines) = Antiquote.range (maps line_content lines)
- | block_range (List {body, ...}) = Antiquote.range (maps line_source (maps block_lines body));
+fun block_range (Par lines) = Antiquote.text_range (maps line_content lines)
+ | block_range (List {body, ...}) = Antiquote.text_range (maps line_source (maps block_lines body));
fun block_indent (List {indent, ...}) = indent
| block_indent (Par (Line {indent, ...} :: _)) = indent
@@ -204,7 +204,7 @@
local
val block_pos = #1 o block_range;
-val item_pos = #1 o Antiquote.range o maps block_source;
+val item_pos = #1 o Antiquote.text_range o maps block_source;
fun line_reports depth (Line {bullet_pos, content, ...}) =
cons (bullet_pos, Markup.markdown_bullet depth) #> append (text_reports content);