simplified positions -- line is also human-readable in generated .tex file;
authorwenzelm
Tue Dec 12 16:12:48 2017 +0100 (17 months ago)
changeset 67188bc7a6455e12a
parent 67187 3457d7d43ee9
child 67189 725897bbabef
simplified positions -- line is also human-readable in generated .tex file;
src/Pure/PIDE/command.ML
src/Pure/PIDE/markup.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	Tue Dec 12 13:34:11 2017 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Tue Dec 12 16:12:48 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, mark_range = false} (Token.input_of cmt); [])
     1.8 +        (Thy_Output.output_text st' {markdown = false, positions = 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/PIDE/markup.ML	Tue Dec 12 13:34:11 2017 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Tue Dec 12 16:12:48 2017 +0100
     2.3 @@ -54,7 +54,6 @@
     2.4    val position_properties': string list
     2.5    val position_properties: string list
     2.6    val positionN: string val position: T
     2.7 -  val rangeN: string
     2.8    val expressionN: string val expression: string -> T
     2.9    val citationN: string val citation: string -> T
    2.10    val pathN: string val path: string -> T
    2.11 @@ -337,8 +336,6 @@
    2.12  
    2.13  val (positionN, position) = markup_elem "position";
    2.14  
    2.15 -val rangeN = "range";
    2.16 -
    2.17  
    2.18  (* expression *)
    2.19  
     3.1 --- a/src/Pure/Thy/document_antiquotations.ML	Tue Dec 12 13:34:11 2017 +0100
     3.2 +++ b/src/Pure/Thy/document_antiquotations.ML	Tue Dec 12 16:12:48 2017 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4  fun control_antiquotation name s1 s2 =
     3.5    Thy_Output.antiquotation name (Scan.lift Args.cartouche_input)
     3.6      (fn {state, ...} =>
     3.7 -      enclose s1 s2 o Thy_Output.output_text state {markdown = false, mark_range = false});
     3.8 +      enclose s1 s2 o Thy_Output.output_text state {markdown = false, positions = false});
     3.9  
    3.10  in
    3.11  
     4.1 --- a/src/Pure/Thy/latex.ML	Tue Dec 12 13:34:11 2017 +0100
     4.2 +++ b/src/Pure/Thy/latex.ML	Tue Dec 12 16:12:48 2017 +0100
     4.3 @@ -15,7 +15,7 @@
     4.4      Symbol.symbol list -> string
     4.5    val output_symbols: Symbol.symbol list -> string
     4.6    val output_syms: string -> string
     4.7 -  val range_output: Position.T -> string -> string
     4.8 +  val line_output: Position.T -> string -> string
     4.9    val output_token: Token.T -> string
    4.10    val begin_delim: string -> string
    4.11    val end_delim: string -> string
    4.12 @@ -170,42 +170,28 @@
    4.13  end;
    4.14  
    4.15  
    4.16 -(* range marker *)
    4.17 -
    4.18 -local
    4.19 -
    4.20 -val marker = "%:%";
    4.21 -
    4.22 -fun detect_marker s =
    4.23 -  size s > 6 andalso String.isPrefix marker s andalso String.isSuffix marker s;
    4.24 -
    4.25 -fun output_prop (a, b) = enclose marker marker (a ^ "=" ^ b);
    4.26 +(* positions *)
    4.27  
    4.28 -fun output_range pos =
    4.29 -  (case (Position.offset_of pos, Position.end_offset_of pos) of
    4.30 -    (NONE, _) => ""
    4.31 -  | (SOME i, NONE) => output_prop (Markup.rangeN, Value.print_int i)
    4.32 -  | (SOME i, SOME j) => output_prop (Markup.rangeN, Value.print_int i ^ ":" ^ Value.print_int j));
    4.33 -
    4.34 -fun range_line head range line =
    4.35 -  if detect_marker line orelse forall_string (fn s => s = " " orelse s = "\t") line then line
    4.36 -  else if head then "%\n" ^ range ^ "\n" ^ line
    4.37 -  else range ^ "\n" ^ line;
    4.38 -
    4.39 -in
    4.40 -
    4.41 -fun range_output pos output =
    4.42 -  (case (output_range pos, split_lines output) of
    4.43 -    (_, []) => ""
    4.44 -  | ("", _ :: _) => output
    4.45 -  | (r, l :: ls) => cat_lines (range_line true r l :: map (range_line false r) ls));
    4.46 +fun output_prop (a, b) = enclose "%:%" "%:%\n" (a ^ "=" ^ b);
    4.47  
    4.48  fun output_file pos =
    4.49    (case Position.file_of pos of
    4.50      NONE => ""
    4.51    | SOME file => output_prop (Markup.fileN, file));
    4.52  
    4.53 -end;
    4.54 +
    4.55 +val is_blank_line = forall_string (fn s => s = " " orelse s = "\t");
    4.56 +
    4.57 +fun line_output pos output =
    4.58 +  (case Position.line_of pos of
    4.59 +    NONE => output
    4.60 +  | SOME n =>
    4.61 +      (case take_prefix is_blank_line (split_lines output) of
    4.62 +        (_, []) => output
    4.63 +      | (blank, rest) =>
    4.64 +          cat_lines blank ^ "%\n" ^
    4.65 +          output_prop (Markup.lineN, Value.print_int n) ^
    4.66 +          cat_lines rest));
    4.67  
    4.68  
    4.69  (* output token *)
    4.70 @@ -250,7 +236,7 @@
    4.71  
    4.72  fun isabelle_theory pos name txt =
    4.73    output_file pos ^
    4.74 -  "\n\\begin{isabellebody}%\n\
    4.75 +  "\\begin{isabellebody}%\n\
    4.76    \\\setisabellecontext{" ^ output_syms name ^ "}%\n" ^ txt ^
    4.77    "%\n\\end{isabellebody}%\n";
    4.78  
     5.1 --- a/src/Pure/Thy/latex.scala	Tue Dec 12 13:34:11 2017 +0100
     5.2 +++ b/src/Pure/Thy/latex.scala	Tue Dec 12 16:12:48 2017 +0100
     5.3 @@ -30,12 +30,7 @@
     5.4    /* generated .tex file */
     5.5  
     5.6    private val File_Pattern = """^%:%file=(.+)%:%$""".r
     5.7 -  private val Range_Pattern2 = """^*%:%range=(\d+):(\d+)%:%$""".r
     5.8 -  private val Range_Pattern1 = """^*%:%range=(\d+)%:%$""".r
     5.9 -  private val marker = "%:%"
    5.10 -
    5.11 -  def detect_marker(s: String): Boolean =
    5.12 -    s.size > 6 && s.startsWith(marker) && s.endsWith(marker)
    5.13 +  private val Line_Pattern = """^*%:%line=(\d+)%:%$""".r
    5.14  
    5.15    def read_tex_file(tex_file: Path): Tex_File =
    5.16      new Tex_File(tex_file, Line.logical_lines(File.read(tex_file)).toArray)
    5.17 @@ -44,52 +39,34 @@
    5.18    {
    5.19      override def toString: String = tex_file.toString
    5.20  
    5.21 -    val source_file: Option[Path] =
    5.22 -      if (tex_lines.length > 0) {
    5.23 +    val source_file: Option[String] =
    5.24 +      if (tex_lines.nonEmpty) {
    5.25          tex_lines(0) match {
    5.26 -          case File_Pattern(file) if Path.is_wellformed(file) && Path.explode(file).is_file =>
    5.27 -            Some(Path.explode(file))
    5.28 +          case File_Pattern(file) => Some(file)
    5.29            case _ => None
    5.30          }
    5.31        }
    5.32        else None
    5.33  
    5.34 -    val source_content: Line.Document =
    5.35 -      source_file match {
    5.36 -        case Some(file) => Line.Document(Symbol.decode(File.read(file)))
    5.37 -        case None => Line.Document.empty
    5.38 -      }
    5.39 -
    5.40 -    lazy val source_chunk: Symbol.Text_Chunk =
    5.41 -      Symbol.Text_Chunk(source_content.text)
    5.42 -
    5.43      private def prev_lines_iterator(l: Int): Iterator[String] =
    5.44 -      if (0 < l && l <= tex_lines.length) Range.inclusive(l - 1, 0, -1).iterator.map(tex_lines(_))
    5.45 +      if (0 < l && l <= tex_lines.length)
    5.46 +        Range.inclusive(l - 1, 0, -1).iterator.map(tex_lines(_))
    5.47        else Iterator.empty
    5.48  
    5.49      def source_position(l: Int): Option[Position.T] =
    5.50        (for {
    5.51          file <- source_file.iterator
    5.52 -        line <- prev_lines_iterator(l)
    5.53 -        if detect_marker(line)
    5.54 -        symbol_range <-
    5.55 -          (line match {
    5.56 -            case Range_Pattern2(Value.Int(i), Value.Int(j)) => Some(Text.Range(i, j))
    5.57 -            case Range_Pattern1(Value.Int(i)) => Some(Text.Range(i, i + 1))
    5.58 +        s <- prev_lines_iterator(l)
    5.59 +        line <-
    5.60 +          (s match {
    5.61 +            case Line_Pattern(Value.Int(line)) => Some(line)
    5.62              case _ => None
    5.63            })
    5.64 -        range <- source_chunk.incorporate(symbol_range)
    5.65        }
    5.66 -      yield {
    5.67 -        Position.Line_File(source_content.position(range.start).line1, file.implode) :::
    5.68 -        Position.Range(symbol_range)
    5.69 -      }).toStream.headOption
    5.70 -
    5.71 -    def tex_position(line: Int): Position.T =
    5.72 -      Position.Line_File(line, tex_file.implode)
    5.73 +      yield { Position.Line_File(line, file) }).toStream.headOption
    5.74  
    5.75      def position(line: Int): Position.T =
    5.76 -      source_position(line) getOrElse tex_position(line)
    5.77 +      source_position(line) getOrElse Position.Line_File(line, tex_file.implode)
    5.78    }
    5.79  
    5.80  
     6.1 --- a/src/Pure/Thy/thy_output.ML	Tue Dec 12 13:34:11 2017 +0100
     6.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Dec 12 16:12:48 2017 +0100
     6.3 @@ -24,7 +24,7 @@
     6.4    val boolean: string -> bool
     6.5    val integer: string -> int
     6.6    val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
     6.7 -  val output_text: Toplevel.state -> {markdown: bool, mark_range: bool} -> Input.source -> string
     6.8 +  val output_text: Toplevel.state -> {markdown: bool, positions: bool} -> Input.source -> string
     6.9    val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
    6.10    val pretty_text: Proof.context -> string -> Pretty.T
    6.11    val pretty_term: Proof.context -> term -> Pretty.T
    6.12 @@ -193,7 +193,7 @@
    6.13  
    6.14  (* output text *)
    6.15  
    6.16 -fun output_text state {markdown, mark_range} source =
    6.17 +fun output_text state {markdown, positions} source =
    6.18    let
    6.19      val is_reported =
    6.20        (case try Toplevel.context_of state of
    6.21 @@ -211,7 +211,7 @@
    6.22      val output_antiquotes =
    6.23        map (fn ant =>
    6.24          eval_antiquote state ant
    6.25 -        |> mark_range ? Latex.range_output (#1 (Antiquote.range [ant]))) #> implode;
    6.26 +        |> positions ? Latex.line_output (#1 (Antiquote.range [ant]))) #> implode;
    6.27  
    6.28      fun output_line line =
    6.29        (if Markdown.line_is_item line then "\\item " else "") ^
    6.30 @@ -265,15 +265,15 @@
    6.31  fun present_token state tok =
    6.32    (case tok of
    6.33      No_Token => ""
    6.34 -  | Basic_Token tok => Latex.output_token tok |> Latex.range_output (Token.pos_of tok)
    6.35 +  | Basic_Token tok => Latex.output_token tok |> Latex.line_output (Token.pos_of tok)
    6.36    | Markup_Token (cmd, source) =>
    6.37        "%\n\\isamarkup" ^ cmd ^ "{" ^
    6.38 -        output_text state {markdown = false, mark_range = true} source ^ "%\n}\n"
    6.39 +        output_text state {markdown = false, positions = true} source ^ "%\n}\n"
    6.40    | Markup_Env_Token (cmd, source) =>
    6.41        Latex.environment ("isamarkup" ^ cmd)
    6.42 -        (output_text state {markdown = true, mark_range = true} source)
    6.43 +        (output_text state {markdown = true, positions = true} source)
    6.44    | Raw_Token source =>
    6.45 -      "%\n" ^ output_text state {markdown = true, mark_range = true} source ^ "\n");
    6.46 +      "%\n" ^ output_text state {markdown = true, positions = true} source ^ "\n");
    6.47  
    6.48  
    6.49  (* command spans *)
    6.50 @@ -673,10 +673,10 @@
    6.51  fun document_command {markdown} (loc, txt) =
    6.52    Toplevel.keep (fn state =>
    6.53      (case loc of
    6.54 -      NONE => ignore (output_text state {markdown = markdown, mark_range = false} txt)
    6.55 +      NONE => ignore (output_text state {markdown = markdown, positions = false} txt)
    6.56      | SOME (_, pos) =>
    6.57          error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
    6.58    Toplevel.present_local_theory loc (fn state =>
    6.59 -    ignore (output_text state {markdown = markdown, mark_range = false} txt));
    6.60 +    ignore (output_text state {markdown = markdown, positions = false} txt));
    6.61  
    6.62  end;