simplified positions -- line is also human-readable in generated .tex file;

--- a/src/Pure/PIDE/command.ML	Tue Dec 12 13:34:11 2017 +0100
+++ b/src/Pure/PIDE/command.ML	Tue Dec 12 16:12:48 2017 +0100
@@ -199,7 +199,7 @@
   Toplevel.setmp_thread_position tr
     (fn () =>
       Outer_Syntax.side_comments span |> maps (fn cmt =>
-        (Thy_Output.output_text st' {markdown = false, mark_range = false} (Token.input_of cmt); [])
+        (Thy_Output.output_text st' {markdown = false, positions = false} (Token.input_of cmt); [])
           handle exn =>
             if Exn.is_interrupt exn then Exn.reraise exn
             else Runtime.exn_messages exn)) ();

--- a/src/Pure/PIDE/markup.ML	Tue Dec 12 13:34:11 2017 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Dec 12 16:12:48 2017 +0100
@@ -54,7 +54,6 @@
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
-  val rangeN: string
   val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
@@ -337,8 +336,6 @@
 
 val (positionN, position) = markup_elem "position";
 
-val rangeN = "range";
-
 
 (* expression *)
 

--- a/src/Pure/Thy/document_antiquotations.ML	Tue Dec 12 13:34:11 2017 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Tue Dec 12 16:12:48 2017 +0100
@@ -45,7 +45,7 @@
 fun control_antiquotation name s1 s2 =
   Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
     (fn {state, ...} =>
-      enclose s1 s2 o Thy_Output.output_text state {markdown = false, mark_range = false});
+      enclose s1 s2 o Thy_Output.output_text state {markdown = false, positions = false});
 
 in
 

--- a/src/Pure/Thy/latex.ML	Tue Dec 12 13:34:11 2017 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Dec 12 16:12:48 2017 +0100
@@ -15,7 +15,7 @@
     Symbol.symbol list -> string
   val output_symbols: Symbol.symbol list -> string
   val output_syms: string -> string
-  val range_output: Position.T -> string -> string
+  val line_output: Position.T -> string -> string
   val output_token: Token.T -> string
   val begin_delim: string -> string
   val end_delim: string -> string
@@ -170,42 +170,28 @@
 end;
 
 
-(* range marker *)
-
-local
-
-val marker = "%:%";
-
-fun detect_marker s =
-  size s > 6 andalso String.isPrefix marker s andalso String.isSuffix marker s;
-
-fun output_prop (a, b) = enclose marker marker (a ^ "=" ^ b);
+(* positions *)
 
-fun output_range pos =
-  (case (Position.offset_of pos, Position.end_offset_of pos) of
-    (NONE, _) => ""
-  | (SOME i, NONE) => output_prop (Markup.rangeN, Value.print_int i)
-  | (SOME i, SOME j) => output_prop (Markup.rangeN, Value.print_int i ^ ":" ^ Value.print_int j));
-
-fun range_line head range line =
-  if detect_marker line orelse forall_string (fn s => s = " " orelse s = "\t") line then line
-  else if head then "%\n" ^ range ^ "\n" ^ line
-  else range ^ "\n" ^ line;
-
-in
-
-fun range_output pos output =
-  (case (output_range pos, split_lines output) of
-    (_, []) => ""
-  | ("", _ :: _) => output
-  | (r, l :: ls) => cat_lines (range_line true r l :: map (range_line false r) ls));
+fun output_prop (a, b) = enclose "%:%" "%:%\n" (a ^ "=" ^ b);
 
 fun output_file pos =
   (case Position.file_of pos of
     NONE => ""
   | SOME file => output_prop (Markup.fileN, file));
 
-end;
+
+val is_blank_line = forall_string (fn s => s = " " orelse s = "\t");
+
+fun line_output pos output =
+  (case Position.line_of pos of
+    NONE => output
+  | SOME n =>
+      (case take_prefix is_blank_line (split_lines output) of
+        (_, []) => output
+      | (blank, rest) =>
+          cat_lines blank ^ "%\n" ^
+          output_prop (Markup.lineN, Value.print_int n) ^
+          cat_lines rest));
 
 
 (* output token *)
@@ -250,7 +236,7 @@
 
 fun isabelle_theory pos name txt =
   output_file pos ^
-  "\n\\begin{isabellebody}%\n\
+  "\\begin{isabellebody}%\n\
   \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
   "%\n\\end{isabellebody}%\n";
 

--- a/src/Pure/Thy/latex.scala	Tue Dec 12 13:34:11 2017 +0100
+++ b/src/Pure/Thy/latex.scala	Tue Dec 12 16:12:48 2017 +0100
@@ -30,12 +30,7 @@
   /* generated .tex file */
 
   private val File_Pattern = """^%:%file=(.+)%:%$""".r
-  private val Range_Pattern2 = """^*%:%range=(\d+):(\d+)%:%$""".r
-  private val Range_Pattern1 = """^*%:%range=(\d+)%:%$""".r
-  private val marker = "%:%"
-
-  def detect_marker(s: String): Boolean =
-    s.size > 6 && s.startsWith(marker) && s.endsWith(marker)
+  private val Line_Pattern = """^*%:%line=(\d+)%:%$""".r
 
   def read_tex_file(tex_file: Path): Tex_File =
     new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray)
@@ -44,52 +39,34 @@
   {
     override def toString: String = tex_file.toString
 
-    val source_file: Option[Path] =
-      if (tex_lines.length > 0) {
+    val source_file: Option[String] =
+      if (tex_lines.nonEmpty) {
         tex_lines(0) match {
-          case File_Pattern(file) if Path.is_wellformed(file) && Path.explode(file).is_file =>
-            Some(Path.explode(file))
+          case File_Pattern(file) => Some(file)
           case _ => None
         }
       }
       else None
 
-    val source_content: Line.Document =
-      source_file match {
-        case Some(file) => Line.Document(Symbol.decode(File.read(file)))
-        case None => Line.Document.empty
-      }
-
-    lazy val source_chunk: Symbol.Text_Chunk =
-      Symbol.Text_Chunk(source_content.text)
-
     private def prev_lines_iterator(l: Int): Iterator[String] =
-      if (0 < l && l <= tex_lines.length) Range.inclusive(l - 1, 0, -1).iterator.map(tex_lines(_))
+      if (0 < l && l <= tex_lines.length)
+        Range.inclusive(l - 1, 0, -1).iterator.map(tex_lines(_))
       else Iterator.empty
 
     def source_position(l: Int): Option[Position.T] =
       (for {
         file <- source_file.iterator
-        line <- prev_lines_iterator(l)
-        if detect_marker(line)
-        symbol_range <-
-          (line match {
-            case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j))
-            case Range_Pattern1(Value.Int(i)) => Some(Text.Range(i, i + 1))
+        s <- prev_lines_iterator(l)
+        line <-
+          (s match {
+            case Line_Pattern(Value.Int(line)) => Some(line)
             case _ => None
           })
-        range <- source_chunk.incorporate(symbol_range)
       }
-      yield {
-        Position.Line_File(source_content.position(range.start).line1, file.implode) :::
-        Position.Range(symbol_range)
-      }).toStream.headOption
-
-    def tex_position(line: Int): Position.T =
-      Position.Line_File(line, tex_file.implode)
+      yield { Position.Line_File(line, file) }).toStream.headOption
 
     def position(line: Int): Position.T =
-      source_position(line) getOrElse tex_position(line)
+      source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
   }
 
 

--- a/src/Pure/Thy/thy_output.ML	Tue Dec 12 13:34:11 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Dec 12 16:12:48 2017 +0100
@@ -24,7 +24,7 @@
   val boolean: string -> bool
   val integer: string -> int
   val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
-  val output_text: Toplevel.state -> {markdown: bool, mark_range: bool} -> Input.source -> string
+  val output_text: Toplevel.state -> {markdown: bool, positions: bool} -> Input.source -> string
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
   val pretty_text: Proof.context -> string -> Pretty.T
   val pretty_term: Proof.context -> term -> Pretty.T
@@ -193,7 +193,7 @@
 
 (* output text *)
 
-fun output_text state {markdown, mark_range} source =
+fun output_text state {markdown, positions} source =
   let
     val is_reported =
       (case try Toplevel.context_of state of
@@ -211,7 +211,7 @@
     val output_antiquotes =
       map (fn ant =>
         eval_antiquote state ant
-        |> mark_range ? Latex.range_output (#1 (Antiquote.range [ant]))) #> implode;
+        |> positions ? Latex.line_output (#1 (Antiquote.range [ant]))) #> implode;
 
     fun output_line line =
       (if Markdown.line_is_item line then "\\item " else "") ^
@@ -265,15 +265,15 @@
 fun present_token state tok =
   (case tok of
     No_Token => ""
-  | Basic_Token tok => Latex.output_token tok |> Latex.range_output (Token.pos_of tok)
+  | Basic_Token tok => Latex.output_token tok |> Latex.line_output (Token.pos_of tok)
   | Markup_Token (cmd, source) =>
       "%\n\\isamarkup" ^ cmd ^ "{" ^
-        output_text state {markdown = false, mark_range = true} source ^ "%\n}\n"
+        output_text state {markdown = false, positions = true} source ^ "%\n}\n"
   | Markup_Env_Token (cmd, source) =>
       Latex.environment ("isamarkup" ^ cmd)
-        (output_text state {markdown = true, mark_range = true} source)
+        (output_text state {markdown = true, positions = true} source)
   | Raw_Token source =>
-      "%\n" ^ output_text state {markdown = true, mark_range = true} source ^ "\n");
+      "%\n" ^ output_text state {markdown = true, positions = true} source ^ "\n");
 
 
 (* command spans *)
@@ -673,10 +673,10 @@
 fun document_command {markdown} (loc, txt) =
   Toplevel.keep (fn state =>
     (case loc of
-      NONE => ignore (output_text state {markdown = markdown, mark_range = false} txt)
+      NONE => ignore (output_text state {markdown = markdown, positions = false} txt)
     | SOME (_, pos) =>
         error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
   Toplevel.present_local_theory loc (fn state =>
-    ignore (output_text state {markdown = markdown, mark_range = false} txt));
+    ignore (output_text state {markdown = markdown, positions = false} txt));
 
 end;