# HG changeset patch
# User wenzelm
# Date 1516357591 -3600
# Node ID 482b62d694ca4c8aed0fc7652f370b5acfd82db6
# Parent  82bc0d5d1ef3dbc53260771ac5e164c86e653934
clarified signature;

diff -r 82bc0d5d1ef3 -r 482b62d694ca src/Pure/General/antiquote.ML
--- 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 *)
diff -r 82bc0d5d1ef3 -r 482b62d694ca src/Pure/Thy/markdown.ML
--- 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);