more robust range on preceding comment-line;
no range for blank lines;
avoid recursive output_text/mark_range;
clarified Latex.output_token (no range) vs. Thy_Output.present_token (with range);

--- a/src/Pure/PIDE/command.ML	Mon Dec 11 17:49:47 2017 +0100
+++ b/src/Pure/PIDE/command.ML	Mon Dec 11 17:52:05 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} (Token.input_of cmt); [])
+        (Thy_Output.output_text st' {markdown = false, mark_range = false} (Token.input_of cmt); [])
           handle exn =>
             if Exn.is_interrupt exn then Exn.reraise exn
             else Runtime.exn_messages exn)) ();

--- a/src/Pure/Thy/document_antiquotations.ML	Mon Dec 11 17:49:47 2017 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Mon Dec 11 17:52:05 2017 +0100
@@ -44,7 +44,8 @@
 
 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});
+    (fn {state, ...} =>
+      enclose s1 s2 o Thy_Output.output_text state {markdown = false, mark_range = false});
 
 in
 

--- a/src/Pure/Thy/latex.ML	Mon Dec 11 17:49:47 2017 +0100
+++ b/src/Pure/Thy/latex.ML	Mon Dec 11 17:52:05 2017 +0100
@@ -15,8 +15,6 @@
     Symbol.symbol list -> string
   val output_symbols: Symbol.symbol list -> string
   val output_syms: string -> string
-  val output_file: Position.T -> string
-  val output_range: Position.T -> string
   val range_output: Position.T -> string -> string
   val output_token: Token.T -> string
   val begin_delim: string -> string
@@ -172,14 +170,16 @@
 end;
 
 
-(* output properties *)
+(* range marker *)
 
-fun output_prop (a, b) = enclose "%:%" "%:%\n" (a ^ "=" ^ b);
+local
 
-fun output_file pos =
-  (case Position.file_of pos of
-    NONE => ""
-  | SOME file => output_prop (Markup.fileN, file));
+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);
 
 fun output_range pos =
   (case (Position.offset_of pos, Position.end_offset_of pos) of
@@ -187,11 +187,25 @@
   | (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_output _ "" = ""
-  | range_output pos output =
-      (case output_range pos of
-        "" => output
-      | range => split_lines output |> map (fn "" => "%\n" | line => line ^ range) |> implode);
+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_file pos =
+  (case Position.file_of pos of
+    NONE => ""
+  | SOME file => output_prop (Markup.fileN, file));
+
+end;
 
 
 (* output token *)
@@ -217,7 +231,7 @@
       else if Token.is_kind Token.Cartouche tok then
         enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
       else output_syms s;
-  in range_output (Token.pos_of tok) output end
+  in output end
   handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 
 
@@ -236,7 +250,7 @@
 
 fun isabelle_theory pos name txt =
   output_file pos ^
-  "\\begin{isabellebody}%\n\
+  "\n\\begin{isabellebody}%\n\
   \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
   "%\n\\end{isabellebody}%\n";
 

--- a/src/Pure/Thy/latex.scala	Mon Dec 11 17:49:47 2017 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Dec 11 17:52:05 2017 +0100
@@ -29,9 +29,13 @@
 
   /* 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 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)
 
   def read_tex_file(tex_file: Path): Tex_File =
     new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray)
@@ -59,12 +63,15 @@
     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(_))
+      else Iterator.empty
+
     def source_position(l: Int): Option[Position.T] =
-      for {
-        file <- source_file
-        if 0 < l && l <= tex_lines.length
-        line = tex_lines(l - 1)
-        if line.endsWith("%:%")
+      (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))
@@ -76,10 +83,10 @@
       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)
+      Position.Line_File(line, tex_file.implode)
 
     def position(line: Int): Position.T =
       source_position(line) getOrElse tex_position(line)

--- a/src/Pure/Thy/thy_output.ML	Mon Dec 11 17:49:47 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML	Mon Dec 11 17:52:05 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} -> Input.source -> string
+  val output_text: Toplevel.state -> {markdown: bool, mark_range: 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
@@ -35,8 +35,8 @@
   val string_of_margin: Proof.context -> Pretty.T -> string
   val output: Proof.context -> Pretty.T list -> string
   val verbatim_text: Proof.context -> string -> string
-  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
-    Toplevel.transition -> Toplevel.transition
+  val document_command: {markdown: bool} ->
+    (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -193,7 +193,7 @@
 
 (* output text *)
 
-fun output_text state {markdown} source =
+fun output_text state {markdown, mark_range} source =
   let
     val is_reported =
       (case try Toplevel.context_of state of
@@ -208,7 +208,11 @@
         Position.report pos (Markup.language_document (Input.is_delimited source))
       else ();
 
-    val output_antiquotes = map (eval_antiquote state) #> implode;
+    val output_antiquotes =
+      map (fn ant =>
+        eval_antiquote state ant
+        |> mark_range ? Latex.range_output (#1 (Antiquote.range [ant])))
+      #> cat_lines;
 
     fun output_line line =
       (if Markdown.line_is_item line then "\\item " else "") ^
@@ -218,24 +222,23 @@
     and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
       | output_block (Markdown.List {kind, body, ...}) =
           Latex.environment (Markdown.print_kind kind) (output_blocks body);
-
-    val output =
-      if Toplevel.is_skipped_proof state then ""
-      else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
-      then
-        let
-          val ants = Antiquote.parse pos syms;
-          val reports = Antiquote.antiq_reports ants;
-          val blocks = Markdown.read_antiquotes ants;
-          val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
-        in output_blocks blocks end
-      else
-        let
-          val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
-          val reports = Antiquote.antiq_reports ants;
-          val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
-        in output_antiquotes ants end;
-  in Latex.range_output pos output end;
+  in
+    if Toplevel.is_skipped_proof state then ""
+    else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
+    then
+      let
+        val ants = Antiquote.parse pos syms;
+        val reports = Antiquote.antiq_reports ants;
+        val blocks = Markdown.read_antiquotes ants;
+        val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
+      in "%\n" ^ output_blocks blocks end
+    else
+      let
+        val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
+        val reports = Antiquote.antiq_reports ants;
+        val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
+      in "%\n" ^ output_antiquotes ants end
+  end;
 
 
 
@@ -260,20 +263,17 @@
 val blank_token = basic_token Token.is_blank;
 val newline_token = basic_token Token.is_newline;
 
-
-(* output token *)
-
-fun output_token state tok =
+fun present_token state tok =
   (case tok of
     No_Token => ""
-  | Basic_Token tok => Latex.output_token tok
+  | Basic_Token tok => Latex.output_token tok |> Latex.range_output (Token.pos_of tok)
   | Markup_Token (cmd, source) =>
-      "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
+      "%\n\\isamarkup" ^ cmd ^ "{" ^
+        output_text state {markdown = false, mark_range = true} source ^ "%\n}\n"
   | Markup_Env_Token (cmd, source) =>
-      Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source)
-  | Raw_Token source =>
-      let val output = "%\n" ^ output_text state {markdown = true} source
-      in if String.isSuffix "\n" output then output else output ^ "\n" end);
+      Latex.environment ("isamarkup" ^ cmd)
+        (output_text state {markdown = true, mark_range = true} source)
+  | Raw_Token source => output_text state {markdown = true, mark_range = true} source ^ "\n");
 
 
 (* command spans *)
@@ -320,7 +320,7 @@
     (tag_stack, active_tag, newline, buffer, present_cont) =
   let
     val present = fold (fn (tok, (flag, 0)) =>
-        Buffer.add (output_token state' tok)
+        Buffer.add (present_token state' tok)
         #> Buffer.add flag
       | _ => I);
 
@@ -670,12 +670,13 @@
 
 (** document command **)
 
-fun document_command markdown (loc, txt) =
+fun document_command {markdown} (loc, txt) =
   Toplevel.keep (fn state =>
     (case loc of
-      NONE => ignore (output_text state markdown txt)
+      NONE => ignore (output_text state {markdown = markdown, mark_range = 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 txt));
+  Toplevel.present_local_theory loc (fn state =>
+    ignore (output_text state {markdown = markdown, mark_range = false} txt));
 
 end;