# HG changeset patch # User wenzelm # Date 1513011125 -3600 # Node ID ecc786cb3b7bc0fbdd1a6c3176b52634471d91d9 # Parent 28227b13a2f1b9d4de9dcd8a939df123f769ffee 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); diff -r 28227b13a2f1 -r ecc786cb3b7b src/Pure/PIDE/command.ML --- 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)) (); diff -r 28227b13a2f1 -r ecc786cb3b7b src/Pure/Thy/document_antiquotations.ML --- 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 diff -r 28227b13a2f1 -r ecc786cb3b7b src/Pure/Thy/latex.ML --- 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"; diff -r 28227b13a2f1 -r ecc786cb3b7b src/Pure/Thy/latex.scala --- 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) diff -r 28227b13a2f1 -r ecc786cb3b7b src/Pure/Thy/thy_output.ML --- 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;