# HG changeset patch # User wenzelm # Date 1513091568 -3600 # Node ID bc7a6455e12afb7ac9e9415962a047658a55b0aa # Parent 3457d7d43ee95e89f16540ce615489fe001b4d3e simplified positions -- line is also human-readable in generated .tex file; diff -r 3457d7d43ee9 -r bc7a6455e12a src/Pure/PIDE/command.ML --- 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)) (); diff -r 3457d7d43ee9 -r bc7a6455e12a src/Pure/PIDE/markup.ML --- 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 *) diff -r 3457d7d43ee9 -r bc7a6455e12a src/Pure/Thy/document_antiquotations.ML --- 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 diff -r 3457d7d43ee9 -r bc7a6455e12a src/Pure/Thy/latex.ML --- 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"; diff -r 3457d7d43ee9 -r bc7a6455e12a src/Pure/Thy/latex.scala --- 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) } diff -r 3457d7d43ee9 -r bc7a6455e12a src/Pure/Thy/thy_output.ML --- 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;