more robust range on preceding comment-line;
authorwenzelm
Mon Dec 11 17:52:05 2017 +0100 (17 months ago)
changeset 67184ecc786cb3b7b
parent 67183 28227b13a2f1
child 67185 d5e51ba21561
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);
src/Pure/PIDE/command.ML
src/Pure/Thy/document_antiquotations.ML
src/Pure/Thy/latex.ML
src/Pure/Thy/latex.scala
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Mon Dec 11 17:49:47 2017 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Mon Dec 11 17:52:05 2017 +0100
     1.3 @@ -199,7 +199,7 @@
     1.4    Toplevel.setmp_thread_position tr
     1.5      (fn () =>
     1.6        Outer_Syntax.side_comments span |> maps (fn cmt =>
     1.7 -        (Thy_Output.output_text st' {markdown = false} (Token.input_of cmt); [])
     1.8 +        (Thy_Output.output_text st' {markdown = false, mark_range = false} (Token.input_of cmt); [])
     1.9            handle exn =>
    1.10              if Exn.is_interrupt exn then Exn.reraise exn
    1.11              else Runtime.exn_messages exn)) ();
     2.1 --- a/src/Pure/Thy/document_antiquotations.ML	Mon Dec 11 17:49:47 2017 +0100
     2.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Mon Dec 11 17:52:05 2017 +0100
     2.3 @@ -44,7 +44,8 @@
     2.4  
     2.5  fun control_antiquotation name s1 s2 =
     2.6    Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
     2.7 -    (fn {state, ...} => enclose s1 s2 o Thy_Output.output_text state {markdown = false});
     2.8 +    (fn {state, ...} =>
     2.9 +      enclose s1 s2 o Thy_Output.output_text state {markdown = false, mark_range = false});
    2.10  
    2.11  in
    2.12  
     3.1 --- a/src/Pure/Thy/latex.ML	Mon Dec 11 17:49:47 2017 +0100
     3.2 +++ b/src/Pure/Thy/latex.ML	Mon Dec 11 17:52:05 2017 +0100
     3.3 @@ -15,8 +15,6 @@
     3.4      Symbol.symbol list -> string
     3.5    val output_symbols: Symbol.symbol list -> string
     3.6    val output_syms: string -> string
     3.7 -  val output_file: Position.T -> string
     3.8 -  val output_range: Position.T -> string
     3.9    val range_output: Position.T -> string -> string
    3.10    val output_token: Token.T -> string
    3.11    val begin_delim: string -> string
    3.12 @@ -172,14 +170,16 @@
    3.13  end;
    3.14  
    3.15  
    3.16 -(* output properties *)
    3.17 +(* range marker *)
    3.18  
    3.19 -fun output_prop (a, b) = enclose "%:%" "%:%\n" (a ^ "=" ^ b);
    3.20 +local
    3.21  
    3.22 -fun output_file pos =
    3.23 -  (case Position.file_of pos of
    3.24 -    NONE => ""
    3.25 -  | SOME file => output_prop (Markup.fileN, file));
    3.26 +val marker = "%:%";
    3.27 +
    3.28 +fun detect_marker s =
    3.29 +  size s > 6 andalso String.isPrefix marker s andalso String.isSuffix marker s;
    3.30 +
    3.31 +fun output_prop (a, b) = enclose marker marker (a ^ "=" ^ b);
    3.32  
    3.33  fun output_range pos =
    3.34    (case (Position.offset_of pos, Position.end_offset_of pos) of
    3.35 @@ -187,11 +187,25 @@
    3.36    | (SOME i, NONE) => output_prop (Markup.rangeN, Value.print_int i)
    3.37    | (SOME i, SOME j) => output_prop (Markup.rangeN, Value.print_int i ^ ":" ^ Value.print_int j));
    3.38  
    3.39 -fun range_output _ "" = ""
    3.40 -  | range_output pos output =
    3.41 -      (case output_range pos of
    3.42 -        "" => output
    3.43 -      | range => split_lines output |> map (fn "" => "%\n" | line => line ^ range) |> implode);
    3.44 +fun range_line head range line =
    3.45 +  if detect_marker line orelse forall_string (fn s => s = " " orelse s = "\t") line then line
    3.46 +  else if head then "%\n" ^ range ^ "\n" ^ line
    3.47 +  else range ^ "\n" ^ line;
    3.48 +
    3.49 +in
    3.50 +
    3.51 +fun range_output pos output =
    3.52 +  (case (output_range pos, split_lines output) of
    3.53 +    (_, []) => ""
    3.54 +  | ("", _ :: _) => output
    3.55 +  | (r, l :: ls) => cat_lines (range_line true r l :: map (range_line false r) ls));
    3.56 +
    3.57 +fun output_file pos =
    3.58 +  (case Position.file_of pos of
    3.59 +    NONE => ""
    3.60 +  | SOME file => output_prop (Markup.fileN, file));
    3.61 +
    3.62 +end;
    3.63  
    3.64  
    3.65  (* output token *)
    3.66 @@ -217,7 +231,7 @@
    3.67        else if Token.is_kind Token.Cartouche tok then
    3.68          enclose "{\\isacartoucheopen}" "{\\isacartoucheclose}" (output_syms s)
    3.69        else output_syms s;
    3.70 -  in range_output (Token.pos_of tok) output end
    3.71 +  in output end
    3.72    handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
    3.73  
    3.74  
    3.75 @@ -236,7 +250,7 @@
    3.76  
    3.77  fun isabelle_theory pos name txt =
    3.78    output_file pos ^
    3.79 -  "\\begin{isabellebody}%\n\
    3.80 +  "\n\\begin{isabellebody}%\n\
    3.81    \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
    3.82    "%\n\\end{isabellebody}%\n";
    3.83  
     4.1 --- a/src/Pure/Thy/latex.scala	Mon Dec 11 17:49:47 2017 +0100
     4.2 +++ b/src/Pure/Thy/latex.scala	Mon Dec 11 17:52:05 2017 +0100
     4.3 @@ -29,9 +29,13 @@
     4.4  
     4.5    /* generated .tex file */
     4.6  
     4.7 -  private val File_Pattern = """^.*%:%file=(.+)%:%$""".r
     4.8 -  private val Range_Pattern2 = """^.*%:%range=(\d+):(\d+)%:%$""".r
     4.9 -  private val Range_Pattern1 = """^.*%:%range=(\d+)%:%$""".r
    4.10 +  private val File_Pattern = """^%:%file=(.+)%:%$""".r
    4.11 +  private val Range_Pattern2 = """^*%:%range=(\d+):(\d+)%:%$""".r
    4.12 +  private val Range_Pattern1 = """^*%:%range=(\d+)%:%$""".r
    4.13 +  private val marker = "%:%"
    4.14 +
    4.15 +  def detect_marker(s: String): Boolean =
    4.16 +    s.size > 6 && s.startsWith(marker) && s.endsWith(marker)
    4.17  
    4.18    def read_tex_file(tex_file: Path): Tex_File =
    4.19      new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray)
    4.20 @@ -59,12 +63,15 @@
    4.21      lazy val source_chunk: Symbol.Text_Chunk =
    4.22        Symbol.Text_Chunk(source_content.text)
    4.23  
    4.24 +    private def prev_lines_iterator(l: Int): Iterator[String] =
    4.25 +      if (0 < l && l <= tex_lines.length) Range.inclusive(l - 1, 0, -1).iterator.map(tex_lines(_))
    4.26 +      else Iterator.empty
    4.27 +
    4.28      def source_position(l: Int): Option[Position.T] =
    4.29 -      for {
    4.30 -        file <- source_file
    4.31 -        if 0 < l && l <= tex_lines.length
    4.32 -        line = tex_lines(l - 1)
    4.33 -        if line.endsWith("%:%")
    4.34 +      (for {
    4.35 +        file <- source_file.iterator
    4.36 +        line <- prev_lines_iterator(l)
    4.37 +        if detect_marker(line)
    4.38          symbol_range <-
    4.39            (line match {
    4.40              case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j))
    4.41 @@ -76,10 +83,10 @@
    4.42        yield {
    4.43          Position.Line_File(source_content.position(range.start).line1, file.implode) :::
    4.44          Position.Range(symbol_range)
    4.45 -      }
    4.46 +      }).toStream.headOption
    4.47  
    4.48      def tex_position(line: Int): Position.T =
    4.49 -        Position.Line_File(line, tex_file.implode)
    4.50 +      Position.Line_File(line, tex_file.implode)
    4.51  
    4.52      def position(line: Int): Position.T =
    4.53        source_position(line) getOrElse tex_position(line)
     5.1 --- a/src/Pure/Thy/thy_output.ML	Mon Dec 11 17:49:47 2017 +0100
     5.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Dec 11 17:52:05 2017 +0100
     5.3 @@ -24,7 +24,7 @@
     5.4    val boolean: string -> bool
     5.5    val integer: string -> int
     5.6    val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
     5.7 -  val output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string
     5.8 +  val output_text: Toplevel.state -> {markdown: bool, mark_range: bool} -> Input.source -> string
     5.9    val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    5.10    val pretty_text: Proof.context -> string -> Pretty.T
    5.11    val pretty_term: Proof.context -> term -> Pretty.T
    5.12 @@ -35,8 +35,8 @@
    5.13    val string_of_margin: Proof.context -> Pretty.T -> string
    5.14    val output: Proof.context -> Pretty.T list -> string
    5.15    val verbatim_text: Proof.context -> string -> string
    5.16 -  val document_command: {markdown: bool} -> (xstring * Position.T) option * Input.source ->
    5.17 -    Toplevel.transition -> Toplevel.transition
    5.18 +  val document_command: {markdown: bool} ->
    5.19 +    (xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
    5.20  end;
    5.21  
    5.22  structure Thy_Output: THY_OUTPUT =
    5.23 @@ -193,7 +193,7 @@
    5.24  
    5.25  (* output text *)
    5.26  
    5.27 -fun output_text state {markdown} source =
    5.28 +fun output_text state {markdown, mark_range} source =
    5.29    let
    5.30      val is_reported =
    5.31        (case try Toplevel.context_of state of
    5.32 @@ -208,7 +208,11 @@
    5.33          Position.report pos (Markup.language_document (Input.is_delimited source))
    5.34        else ();
    5.35  
    5.36 -    val output_antiquotes = map (eval_antiquote state) #> implode;
    5.37 +    val output_antiquotes =
    5.38 +      map (fn ant =>
    5.39 +        eval_antiquote state ant
    5.40 +        |> mark_range ? Latex.range_output (#1 (Antiquote.range [ant])))
    5.41 +      #> cat_lines;
    5.42  
    5.43      fun output_line line =
    5.44        (if Markdown.line_is_item line then "\\item " else "") ^
    5.45 @@ -218,24 +222,23 @@
    5.46      and output_block (Markdown.Par lines) = cat_lines (map output_line lines)
    5.47        | output_block (Markdown.List {kind, body, ...}) =
    5.48            Latex.environment (Markdown.print_kind kind) (output_blocks body);
    5.49 -
    5.50 -    val output =
    5.51 -      if Toplevel.is_skipped_proof state then ""
    5.52 -      else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
    5.53 -      then
    5.54 -        let
    5.55 -          val ants = Antiquote.parse pos syms;
    5.56 -          val reports = Antiquote.antiq_reports ants;
    5.57 -          val blocks = Markdown.read_antiquotes ants;
    5.58 -          val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
    5.59 -        in output_blocks blocks end
    5.60 -      else
    5.61 -        let
    5.62 -          val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
    5.63 -          val reports = Antiquote.antiq_reports ants;
    5.64 -          val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
    5.65 -        in output_antiquotes ants end;
    5.66 -  in Latex.range_output pos output end;
    5.67 +  in
    5.68 +    if Toplevel.is_skipped_proof state then ""
    5.69 +    else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
    5.70 +    then
    5.71 +      let
    5.72 +        val ants = Antiquote.parse pos syms;
    5.73 +        val reports = Antiquote.antiq_reports ants;
    5.74 +        val blocks = Markdown.read_antiquotes ants;
    5.75 +        val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
    5.76 +      in "%\n" ^ output_blocks blocks end
    5.77 +    else
    5.78 +      let
    5.79 +        val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
    5.80 +        val reports = Antiquote.antiq_reports ants;
    5.81 +        val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
    5.82 +      in "%\n" ^ output_antiquotes ants end
    5.83 +  end;
    5.84  
    5.85  
    5.86  
    5.87 @@ -260,20 +263,17 @@
    5.88  val blank_token = basic_token Token.is_blank;
    5.89  val newline_token = basic_token Token.is_newline;
    5.90  
    5.91 -
    5.92 -(* output token *)
    5.93 -
    5.94 -fun output_token state tok =
    5.95 +fun present_token state tok =
    5.96    (case tok of
    5.97      No_Token => ""
    5.98 -  | Basic_Token tok => Latex.output_token tok
    5.99 +  | Basic_Token tok => Latex.output_token tok |> Latex.range_output (Token.pos_of tok)
   5.100    | Markup_Token (cmd, source) =>
   5.101 -      "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text state {markdown = false} source ^ "%\n}\n"
   5.102 +      "%\n\\isamarkup" ^ cmd ^ "{" ^
   5.103 +        output_text state {markdown = false, mark_range = true} source ^ "%\n}\n"
   5.104    | Markup_Env_Token (cmd, source) =>
   5.105 -      Latex.environment ("isamarkup" ^ cmd) (output_text state {markdown = true} source)
   5.106 -  | Raw_Token source =>
   5.107 -      let val output = "%\n" ^ output_text state {markdown = true} source
   5.108 -      in if String.isSuffix "\n" output then output else output ^ "\n" end);
   5.109 +      Latex.environment ("isamarkup" ^ cmd)
   5.110 +        (output_text state {markdown = true, mark_range = true} source)
   5.111 +  | Raw_Token source => output_text state {markdown = true, mark_range = true} source ^ "\n");
   5.112  
   5.113  
   5.114  (* command spans *)
   5.115 @@ -320,7 +320,7 @@
   5.116      (tag_stack, active_tag, newline, buffer, present_cont) =
   5.117    let
   5.118      val present = fold (fn (tok, (flag, 0)) =>
   5.119 -        Buffer.add (output_token state' tok)
   5.120 +        Buffer.add (present_token state' tok)
   5.121          #> Buffer.add flag
   5.122        | _ => I);
   5.123  
   5.124 @@ -670,12 +670,13 @@
   5.125  
   5.126  (** document command **)
   5.127  
   5.128 -fun document_command markdown (loc, txt) =
   5.129 +fun document_command {markdown} (loc, txt) =
   5.130    Toplevel.keep (fn state =>
   5.131      (case loc of
   5.132 -      NONE => ignore (output_text state markdown txt)
   5.133 +      NONE => ignore (output_text state {markdown = markdown, mark_range = false} txt)
   5.134      | SOME (_, pos) =>
   5.135          error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
   5.136 -  Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt));
   5.137 +  Toplevel.present_local_theory loc (fn state =>
   5.138 +    ignore (output_text state {markdown = markdown, mark_range = false} txt));
   5.139  
   5.140  end;