# HG changeset patch # User wenzelm # Date 1516385365 -3600 # Node ID 90def2b0630594a848c44ea01d15fac3768ceb7a # Parent aad088768872c9dc985ad8ed543ad8ba366300a6 more uniform output of source / text / theory_text, with handling of formal comments etc.; diff -r aad088768872 -r 90def2b06305 src/Pure/Thy/document_antiquotation.ML --- a/src/Pure/Thy/document_antiquotation.ML Fri Jan 19 15:20:13 2018 +0100 +++ b/src/Pure/Thy/document_antiquotation.ML Fri Jan 19 19:09:25 2018 +0100 @@ -16,6 +16,7 @@ val trim_blanks: Proof.context -> string -> string val trim_lines: Proof.context -> string -> string val indent_lines: Proof.context -> string -> string + val prepare_lines: Proof.context -> string -> string val quote: Proof.context -> Pretty.T -> Pretty.T val indent: Proof.context -> Pretty.T -> Pretty.T val format: Proof.context -> Pretty.T -> string @@ -60,6 +61,8 @@ prefix_lines (Symbol.spaces (Config.get ctxt thy_output_indent)) else I; +fun prepare_lines ctxt = trim_lines ctxt #> indent_lines ctxt; + (* output *) diff -r aad088768872 -r 90def2b06305 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Fri Jan 19 15:20:13 2018 +0100 +++ b/src/Pure/Thy/document_antiquotations.ML Fri Jan 19 19:09:25 2018 +0100 @@ -150,51 +150,56 @@ local +fun report_text ctxt text = + Context_Position.report ctxt (Input.pos_of text) + (Markup.language_text (Input.is_delimited text)); + +fun prepare_text ctxt = + Input.source_content #> Document_Antiquotation.prepare_lines ctxt; + fun text_antiquotation name = Thy_Output.antiquotation_raw name (Scan.lift Args.text_input) (fn ctxt => fn text => let + val _ = report_text ctxt text; + in + prepare_text ctxt text + |> Thy_Output.output_source ctxt + |> Thy_Output.isabelle ctxt + end); + +val theory_text_antiquotation = + Thy_Output.antiquotation_raw \<^binding>\theory_text\ (Scan.lift Args.text_input) + (fn ctxt => fn text => + let + val keywords = Thy_Header.get_keywords' ctxt; + + val _ = report_text ctxt text; val _ = - Context_Position.report ctxt (Input.pos_of text) - (Markup.language_text (Input.is_delimited text)); - in Thy_Output.pretty ctxt [Thy_Output.pretty_text ctxt (Input.source_content text)] end); + Input.source_explode text + |> Source.of_list + |> Token.source' true keywords + |> Source.exhaust + |> maps (Token.reports keywords) + |> Context_Position.reports_text ctxt; + in + prepare_text ctxt text + |> Token.explode keywords Position.none + |> maps (Thy_Output.output_token ctxt) + |> Thy_Output.isabelle ctxt + end); in val _ = Theory.setup (text_antiquotation \<^binding>\text\ #> - text_antiquotation \<^binding>\cartouche\); + text_antiquotation \<^binding>\cartouche\ #> + theory_text_antiquotation); end; -(* theory text with tokens (unchecked) *) - -val _ = - Theory.setup - (Thy_Output.antiquotation_raw \<^binding>\theory_text\ (Scan.lift Args.text_input) - (fn ctxt => fn text => - let - val keywords = Thy_Header.get_keywords' ctxt; - - val _ = - Context_Position.report ctxt (Input.pos_of text) - (Markup.language_Isar (Input.is_delimited text)); - val _ = - Input.source_explode text - |> Source.of_list - |> Token.source' true keywords - |> Source.exhaust - |> maps (Token.reports keywords) - |> Context_Position.reports_text ctxt; - - val toks = - Input.source_content text - |> Document_Antiquotation.trim_lines ctxt - |> Document_Antiquotation.indent_lines ctxt - |> Token.explode keywords Position.none; - in Thy_Output.isabelle ctxt (maps (Thy_Output.output_token ctxt) toks) end)); (* goal state *) diff -r aad088768872 -r 90def2b06305 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Jan 19 15:20:13 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Fri Jan 19 19:09:25 2018 +0100 @@ -10,9 +10,9 @@ val check_comments: Proof.context -> Symbol_Pos.T list -> unit val check_token_comments: Proof.context -> Token.T -> unit val output_token: Proof.context -> Token.T -> Latex.text list + val output_source: Proof.context -> string -> Latex.text list val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Latex.text list - val pretty_text: Proof.context -> string -> Pretty.T val pretty_term: Proof.context -> term -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val lines: Latex.text list -> Latex.text list @@ -20,6 +20,7 @@ val isabelle_typewriter: Proof.context -> Latex.text list -> Latex.text val typewriter: Proof.context -> string -> Latex.text val verbatim: Proof.context -> string -> Latex.text + val source: Proof.context -> Token.src -> Latex.text val pretty: Proof.context -> Pretty.T list -> Latex.text val pretty_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text val antiquotation_pretty: @@ -133,6 +134,9 @@ | _ => output false "" "") end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); +fun output_source ctxt s = + output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none)); + fun check_comments ctxt = Comment.read_body #> (Option.app o List.app) (fn (comment, syms) => let @@ -430,9 +434,6 @@ (* pretty printing *) -fun pretty_text ctxt = - Pretty.chunks o map (Pretty.str o Document_Antiquotation.trim_blanks ctxt) o split_lines; - fun pretty_term ctxt t = Syntax.pretty_term (Variable.auto_fixes t ctxt) t; @@ -461,13 +462,19 @@ then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt else split_lines #> map (typewriter ctxt) #> lines #> Latex.block; +fun source ctxt = + Token.args_of_src + #> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt) + #> space_implode " " + #> output_source ctxt + #> isabelle ctxt; + fun pretty ctxt = map (Document_Antiquotation.output ctxt #> Latex.string) #> lines #> isabelle ctxt; fun pretty_source ctxt src prts = - if Config.get ctxt Document_Antiquotation.thy_output_source then - pretty ctxt [pretty_text ctxt (space_implode " " (map Token.unparse (Token.args_of_src src)))] - else pretty ctxt prts; + if Config.get ctxt Document_Antiquotation.thy_output_source + then source ctxt src else pretty ctxt prts; (* antiquotation variants *)