# HG changeset patch # User wenzelm # Date 1447187474 -3600 # Node ID f22054b192b0475fe3954112c5b90f388d1e4d4d # Parent 27af754f50ca9f9546746512c1441763b3f80b50 clarified modules; diff -r 27af754f50ca -r f22054b192b0 src/Pure/ROOT --- a/src/Pure/ROOT Tue Nov 10 20:49:48 2015 +0100 +++ b/src/Pure/ROOT Tue Nov 10 21:31:14 2015 +0100 @@ -227,6 +227,7 @@ "System/message_channel.ML" "System/options.ML" "System/system_channel.ML" + "Thy/document_antiquotations.ML" "Thy/html.ML" "Thy/latex.ML" "Thy/markdown.ML" diff -r 27af754f50ca -r f22054b192b0 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Nov 10 20:49:48 2015 +0100 +++ b/src/Pure/ROOT.ML Tue Nov 10 21:31:14 2015 +0100 @@ -303,6 +303,7 @@ use "Thy/term_style.ML"; use "Isar/outer_syntax.ML"; use "Thy/thy_output.ML"; +use "Thy/document_antiquotations.ML"; use "General/graph_display.ML"; use "Thy/present.ML"; use "pure_syn.ML"; diff -r 27af754f50ca -r f22054b192b0 src/Pure/Thy/document_antiquotations.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/document_antiquotations.ML Tue Nov 10 21:31:14 2015 +0100 @@ -0,0 +1,175 @@ +(* Title: Pure/ML/document_antiquotations.ML + Author: Makarius + +Miscellaneous document antiquotations. +*) + +structure Document_Antiquotations: sig end = +struct + +(* control spacing *) + +val _ = + Theory.setup + (Thy_Output.antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #> + Thy_Output.antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #> + Thy_Output.antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #> + Thy_Output.antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip")); + + +(* control style *) + +local + +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}); + +in + +val _ = + Theory.setup + (control_antiquotation @{binding footnote} "\\footnote{" "}" #> + control_antiquotation @{binding emph} "\\emph{" "}" #> + control_antiquotation @{binding bold} "\\textbf{" "}"); + +end; + + +(* quasi-formal text (unchecked) *) + +local + +fun text_antiquotation name = + Thy_Output.antiquotation name (Scan.lift Args.text_input) + (fn {context = ctxt, ...} => fn source => + (Context_Position.report ctxt (Input.pos_of source) + (Markup.language_text (Input.is_delimited source)); + Thy_Output.output ctxt [Thy_Output.pretty_text ctxt (Input.source_content source)])); + +in + +val _ = + Theory.setup + (text_antiquotation @{binding text} #> + text_antiquotation @{binding cartouche}); + +end; + + +(* theory text with tokens (unchecked) *) + +val _ = + Theory.setup + (Thy_Output.antiquotation @{binding theory_text} (Scan.lift Args.text_input) + (fn {context = ctxt, ...} => fn source => + let + val _ = + Context_Position.report ctxt (Input.pos_of source) + (Markup.language_outer (Input.is_delimited source)); + + val keywords = Thy_Header.get_keywords' ctxt; + val toks = + Source.of_list (Input.source_explode source) + |> Token.source' true keywords + |> Source.exhaust; + val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks); + in + implode (map Latex.output_token toks) |> + (if Config.get ctxt Thy_Output.display + then Latex.environment "isabelle" + else enclose "\\isa{" "}") + end)); + + +(* goal state *) + +local + +fun goal_state name main = Thy_Output.antiquotation name (Scan.succeed ()) + (fn {state, context = ctxt, ...} => fn () => + Thy_Output.output ctxt + [Goal_Display.pretty_goal + (Config.put Goal_Display.show_main_goal main ctxt) + (#goal (Proof.goal (Toplevel.proof_of state)))]); + +in + +val _ = Theory.setup + (goal_state @{binding goals} true #> + goal_state @{binding subgoals} false); + +end; + + +(* embedded lemma *) + +val _ = Theory.setup + (Thy_Output.antiquotation @{binding lemma} + (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- + Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) + (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) => + let + val prop_src = Token.src (Token.name_of_src source) [prop_token]; + + val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2); + val _ = Context_Position.reports ctxt reports; + + (* FIXME check proof!? *) + val _ = ctxt + |> Proof.theorem NONE (K I) [[(prop, [])]] + |> Proof.global_terminal_proof (m1, m2); + in + Thy_Output.output ctxt + (Thy_Output.maybe_pretty_source Thy_Output.pretty_term ctxt prop_src [prop]) + end)); + + +(* verbatim text *) + +val _ = + Theory.setup + (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text) + (Thy_Output.verbatim_text o #context)); + + +(* ML text *) + +local + +fun ml_text name ml = Thy_Output.antiquotation name (Scan.lift Args.text_input) + (fn {context = ctxt, ...} => fn source => + (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source); + Thy_Output.verbatim_text ctxt (Input.source_content source))); + +fun ml_enclose bg en source = + ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en; + +in + +val _ = Theory.setup + (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #> + ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #> + ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #> + ml_text @{binding ML_structure} + (ml_enclose "functor XXX() = struct structure XX = " " end;") #> + + ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *) + (fn source => + ML_Lex.read ("ML_Env.check_functor " ^ + ML_Syntax.print_string (Input.source_content source))) #> + + ml_text @{binding ML_text} (K [])); + +end; + + +(* URLs *) + +val _ = Theory.setup + (Thy_Output.antiquotation @{binding url} (Scan.lift (Parse.position Parse.name)) + (fn {context = ctxt, ...} => fn (name, pos) => + (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)]; + enclose "\\url{" "}" name))); + +end; diff -r 27af754f50ca -r f22054b192b0 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Nov 10 20:49:48 2015 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Nov 10 21:31:14 2015 +0100 @@ -597,83 +597,18 @@ #> enclose "\\isa{" "}"); - -(** concrete antiquotations **) - -(* control spacing *) - -val _ = - Theory.setup - (antiquotation @{binding noindent} (Scan.succeed ()) (fn _ => fn () => "\\noindent") #> - antiquotation @{binding smallskip} (Scan.succeed ()) (fn _ => fn () => "\\smallskip") #> - antiquotation @{binding medskip} (Scan.succeed ()) (fn _ => fn () => "\\medskip") #> - antiquotation @{binding bigskip} (Scan.succeed ()) (fn _ => fn () => "\\bigskip")); - - -(* control style *) +(* verbatim text *) -local - -fun control_antiquotation name s1 s2 = - antiquotation name (Scan.lift Args.cartouche_input) - (fn {state, ...} => enclose s1 s2 o output_text state {markdown = false}); - -in - -val _ = - Theory.setup - (control_antiquotation @{binding footnote} "\\footnote{" "}" #> - control_antiquotation @{binding emph} "\\emph{" "}" #> - control_antiquotation @{binding bold} "\\textbf{" "}"); - -end; +fun verbatim_text ctxt = + if Config.get ctxt display then + Latex.output_ascii #> Latex.environment "isabellett" + else + split_lines #> + map (Latex.output_ascii #> enclose "\\isatt{" "}") #> + space_implode "\\isasep\\isanewline%\n"; -(* quasi-formal text (unchecked) *) - -local - -fun text_antiquotation name = - antiquotation name (Scan.lift Args.text_input) - (fn {context = ctxt, ...} => fn source => - (Context_Position.report ctxt (Input.pos_of source) - (Markup.language_text (Input.is_delimited source)); - output ctxt [pretty_text ctxt (Input.source_content source)])); - -in - -val _ = - Theory.setup - (text_antiquotation @{binding text} #> - text_antiquotation @{binding cartouche}); - -end; - - -(* theory text with tokens (unchecked) *) - -val _ = - Theory.setup - (antiquotation @{binding theory_text} (Scan.lift Args.text_input) - (fn {context = ctxt, ...} => fn source => - let - val _ = - Context_Position.report ctxt (Input.pos_of source) - (Markup.language_outer (Input.is_delimited source)); - - val keywords = Thy_Header.get_keywords' ctxt; - val toks = - Source.of_list (Input.source_explode source) - |> Token.source' true keywords - |> Source.exhaust; - val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks); - in - implode (map Latex.output_token toks) - |> (if Config.get ctxt display then Latex.environment "isabelle" else enclose "\\isa{" "}") - end)); - - -(* basic entities *) +(* antiquotations for basic entities *) local @@ -708,101 +643,6 @@ end; -(* goal state *) - -local - -fun goal_state name main = antiquotation name (Scan.succeed ()) - (fn {state, context = ctxt, ...} => fn () => - output ctxt - [Goal_Display.pretty_goal - (Config.put Goal_Display.show_main_goal main ctxt) - (#goal (Proof.goal (Toplevel.proof_of state)))]); - -in - -val _ = Theory.setup - (goal_state @{binding goals} true #> - goal_state @{binding subgoals} false); - -end; - - -(* embedded lemma *) - -val _ = Theory.setup - (antiquotation @{binding lemma} - (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- - Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) - (fn {source, context = ctxt, ...} => fn ((prop_token, prop), (((_, by_pos), m1), m2)) => - let - val prop_src = Token.src (Token.name_of_src source) [prop_token]; - - val reports = (by_pos, Markup.keyword1) :: maps Method.reports_of (m1 :: the_list m2); - val _ = Context_Position.reports ctxt reports; - - (* FIXME check proof!? *) - val _ = ctxt - |> Proof.theorem NONE (K I) [[(prop, [])]] - |> Proof.global_terminal_proof (m1, m2); - in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end)); - - -(* verbatim text *) - -fun verbatim_text ctxt = - if Config.get ctxt display then - Latex.output_ascii #> Latex.environment "isabellett" - else - split_lines #> - map (Latex.output_ascii #> enclose "\\isatt{" "}") #> - space_implode "\\isasep\\isanewline%\n"; - -val _ = - Theory.setup - (antiquotation @{binding verbatim} (Scan.lift Args.text) (verbatim_text o #context)); - - -(* ML text *) - -local - -fun ml_text name ml = antiquotation name (Scan.lift Args.text_input) - (fn {context = ctxt, ...} => fn source => - (ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of source) (ml source); - verbatim_text ctxt (Input.source_content source))); - -fun ml_enclose bg en source = - ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en; - -in - -val _ = Theory.setup - (ml_text @{binding ML} (ml_enclose "fn _ => (" ");") #> - ml_text @{binding ML_op} (ml_enclose "fn _ => (op " ");") #> - ml_text @{binding ML_type} (ml_enclose "val _ = NONE : (" ") option;") #> - ml_text @{binding ML_structure} - (ml_enclose "functor XXX() = struct structure XX = " " end;") #> - - ml_text @{binding ML_functor} (* FIXME formal treatment of functor name (!?) *) - (fn source => - ML_Lex.read ("ML_Env.check_functor " ^ - ML_Syntax.print_string (Input.source_content source))) #> - - ml_text @{binding ML_text} (K [])); - -end; - - -(* URLs *) - -val _ = Theory.setup - (antiquotation @{binding url} (Scan.lift (Parse.position Parse.name)) - (fn {context = ctxt, ...} => fn (name, pos) => - (Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url name)]; - enclose "\\url{" "}" name))); - - (** document commands **)