# HG changeset patch # User wenzelm # Date 1637679969 -3600 # Node ID fe9e590ae52f56c643ffcf43eb6be72437e1a807 # Parent c299abcf7081c53c6cb591a364767c652d500902 output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction; diff -r c299abcf7081 -r fe9e590ae52f src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Tue Nov 23 12:29:09 2021 +0100 +++ b/src/Pure/Isar/token.ML Tue Nov 23 16:06:09 2021 +0100 @@ -31,7 +31,8 @@ Fact of string option * thm list | Attribute of morphism -> attribute | Declaration of declaration | - Files of file Exn.result list + Files of file Exn.result list | + Output of XML.body option val pos_of: T -> Position.T val adjust_offsets: (int -> int option) -> T -> T val eof: T @@ -73,6 +74,8 @@ val file_source: file -> Input.source val get_files: T -> file Exn.result list val put_files: file Exn.result list -> T -> T + val get_output: T -> XML.body option + val put_output: XML.body -> T -> T val get_value: T -> value option val reports_of_value: T -> Position.report list val name_value: name_value -> value @@ -197,7 +200,8 @@ Fact of string option * thm list | (*optional name for dynamic fact, i.e. fact "variable"*) Attribute of morphism -> attribute | Declaration of declaration | - Files of file Exn.result list; + Files of file Exn.result list | + Output of XML.body option; type src = T list; @@ -411,6 +415,15 @@ | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok)); +(* document output *) + +fun get_output (Token (_, _, Value (SOME (Output output)))) = output + | get_output _ = NONE; + +fun put_output output (Token (x, y, Slot)) = Token (x, y, Value (SOME (Output (SOME output)))) + | put_output _ tok = raise Fail ("Cannot put document output here" ^ Position.here (pos_of tok)); + + (* access values *) fun get_value (Token (_, _, Value v)) = v @@ -491,7 +504,8 @@ | Fact (a, ths) => Fact (a, Morphism.fact phi ths) | Attribute att => Attribute (Morphism.transform phi att) | Declaration decl => Declaration (Morphism.transform phi decl) - | Files _ => v)); + | Files _ => v + | Output _ => v)); (* static binding *) diff -r c299abcf7081 -r fe9e590ae52f src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Tue Nov 23 12:29:09 2021 +0100 +++ b/src/Pure/Isar/toplevel.ML Tue Nov 23 16:06:09 2021 +0100 @@ -17,6 +17,7 @@ val is_skipped_proof: state -> bool val level: state -> int val previous_theory_of: state -> theory option + val output_of: state -> Latex.text option val context_of: state -> Proof.context val generic_theory_of: state -> generic_theory val theory_of: state -> theory @@ -139,20 +140,20 @@ fun node_presentation node = (node, cases_node init_presentation Context.proof_of Proof.context_of node); - datatype state = - State of node_presentation * theory option; - (*current node with presentation context, previous theory*) + State of node_presentation * (theory option * Latex.text option); + (*current node with presentation context, previous theory, document output*) fun node_of (State ((node, _), _)) = node; -fun previous_theory_of (State (_, prev_thy)) = prev_thy; +fun previous_theory_of (State (_, (prev_thy, _))) = prev_thy; +fun output_of (State (_, (_, output))) = output; -fun init_toplevel () = State (node_presentation Toplevel, NONE); -fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE); +fun init_toplevel () = State (node_presentation Toplevel, (NONE, NONE)); +fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), (NONE, NONE)); val prev_theory = Config.declare_int ("prev_theory", Position.none) (K 0); fun get_prev_theory thy = Config.get_global thy prev_theory; -fun set_prev_theory (State (_, SOME prev_thy)) (Theory gthy) = +fun set_prev_theory (State (_, (SOME prev_thy, _))) (Theory gthy) = let val put = Config.put_global prev_theory (Context.theory_identifier prev_thy); val gthy' = gthy |> Context.mapping put (Local_Theory.raw_theory put); @@ -204,10 +205,10 @@ Proof (prf, _) => Proof_Node.position prf | _ => ~1); -fun is_end_theory (State ((Toplevel, _), SOME _)) = true +fun is_end_theory (State ((Toplevel, _), (SOME _, _))) = true | is_end_theory _ = false; -fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy +fun end_theory _ (State ((Toplevel, _), (SOME thy, _))) = thy | end_theory pos _ = error ("Malformed theory" ^ Position.here pos); @@ -223,11 +224,11 @@ fun presentation_context (state as State (current, _)) = presentation_context0 state - |> Presentation_State.put (SOME (State (current, NONE))); + |> Presentation_State.put (SOME (State (current, (NONE, NONE)))); fun presentation_state ctxt = (case Presentation_State.get ctxt of - NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE) + NONE => State (node_presentation (Theory (Context.Proof ctxt)), (NONE, NONE)) | SOME state => state); @@ -286,28 +287,29 @@ exception FAILURE of state * exn; +fun apply_presentation g (st as State (node, (prev_thy, _))) = + State (node, (prev_thy, g st)); + fun apply f g node = let val node_pr = node_presentation node; val context = cases_proper_node I (Context.Proof o Proof.context_of) node; - fun state_error e node_pr' = (State (node_pr', get_theory node), e); + fun make_state node_pr' = State (node_pr', (get_theory node, NONE)); - val (result, err) = - node - |> Runtime.controlled_execution (SOME context) f - |> state_error NONE - handle exn => state_error (SOME exn) node_pr; + val (st', err) = + (Runtime.controlled_execution (SOME context) (f #> make_state #> apply_presentation g) node, + NONE) handle exn => (make_state node_pr, SOME exn); in (case err of - NONE => tap g result - | SOME exn => raise FAILURE (result, exn)) + NONE => st' + | SOME exn => raise FAILURE (st', exn)) end; fun apply_tr int trans state = (case (trans, node_of state) of (Init f, Toplevel) => Runtime.controlled_execution NONE (fn () => - State (node_presentation (Theory (Context.Theory (f ()))), NONE)) () + State (node_presentation (Theory (Context.Theory (f ()))), (NONE, NONE))) () | (Exit, node as Theory (Context.Theory thy)) => let val State ((node', pr_ctxt), _) = @@ -315,11 +317,15 @@ (fn _ => node_presentation (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy))))) - (K ()); - in State ((Toplevel, pr_ctxt), get_theory node') end + no_presentation; + in State ((Toplevel, pr_ctxt), (get_theory node', NONE)) end | (Keep f, node) => Runtime.controlled_execution (try generic_theory_of state) - (fn () => (f int state; State (node_presentation node, previous_theory_of state))) () + (fn () => + let + val prev_thy = previous_theory_of state; + val state' = State (node_presentation node, (prev_thy, NONE)); + in apply_presentation (fn st => f int st) state' end) () | (Transaction _, Toplevel) => raise UNDEF | (Transaction (f, g), node) => apply (fn x => f int x) g (set_prev_theory state node) | _ => raise UNDEF); diff -r c299abcf7081 -r fe9e590ae52f src/Pure/Thy/document_output.ML --- a/src/Pure/Thy/document_output.ML Tue Nov 23 12:29:09 2021 +0100 +++ b/src/Pure/Thy/document_output.ML Tue Nov 23 16:06:09 2021 +0100 @@ -207,9 +207,8 @@ datatype token = Ignore | Token of Token.T - | Heading of Markup.T * Input.source - | Body of Markup.T * Input.source - | Raw of Input.source; + | Markup of Markup.T * Latex.text + | Raw of Latex.text; fun token_with pred (Token tok) = pred tok | token_with _ _ = false; @@ -223,16 +222,14 @@ (case tok of Ignore => [] | Token tok => output_token ctxt tok - | Heading (markup, source) => [XML.Elem (markup, output_document ctxt {markdown = false} source)] - | Body (markup, source) => [XML.Elem (markup, output_document ctxt {markdown = true} source)] - | Raw source => - Latex.string "%\n" @ output_document ctxt {markdown = true} source @ Latex.string "\n"); + | Markup (markup, output) => [XML.Elem (markup, output)] + | Raw output => Latex.enclose_text "%\n" "\n" output); fun mk_heading (kind, pos) source = - Heading (Markup.latex_heading kind |> Position.markup pos, source); + Markup (Markup.latex_heading kind |> Position.markup pos, source); fun mk_body (kind, pos) source = - Body (Markup.latex_body kind |> Position.markup pos, source); + Markup (Markup.latex_body kind |> Position.markup pos, source); (* command spans *) @@ -374,8 +371,30 @@ (* present_thy *) +type segment = + {span: Command_Span.span, command: Toplevel.transition, + prev_state: Toplevel.state, state: Toplevel.state}; + local +fun command_output output tok = + if Token.is_command tok then SOME (Token.put_output output tok) else NONE; + +fun segment_content (segment: segment) = + let val toks = Command_Span.content (#span segment) in + (case Toplevel.output_of (#state segment) of + NONE => toks + | SOME output => map_filter (command_output output) toks) + end; + +fun output_command is_kind = + Scan.some (fn tok => + let val kind = Token.content_of tok in + if Token.is_command tok andalso is_kind kind andalso is_some (Token.get_output tok) + then SOME ((kind, Token.pos_of tok), the (Token.get_output tok)) + else NONE + end); + val markup_true = "\\isamarkuptrue%\n"; val markup_false = "\\isamarkupfalse%\n"; @@ -395,10 +414,6 @@ in -type segment = - {span: Command_Span.span, command: Toplevel.transition, - prev_state: Toplevel.state, state: Toplevel.state}; - fun present_thy options thy (segments: segment list) = let val keywords = Thy_Header.get_keywords thy; @@ -410,16 +425,8 @@ >> (fn d => (NONE, (Ignore, ("", d)))); fun markup pred mk flag = Scan.peek (fn d => - Document_Source.improper |-- - Scan.one (fn tok => Token.is_command tok andalso pred keywords (Token.content_of tok)) -- - (Document_Source.annotation |-- - Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |-- - Parse.document_source --| Document_Source.improper_end)) - >> (fn (tok, source) => - let - val kind = Token.content_of tok; - val pos' = Token.pos_of tok; - in (SOME (kind, pos'), (mk (kind, pos') source, (flag, d))) end)); + Document_Source.improper |-- output_command (pred keywords) --| Document_Source.improper_end + >> (fn (kind, body) => (SOME kind, (mk kind body, (flag, d))))); val command = Scan.peek (fn d => Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] -- @@ -468,7 +475,7 @@ make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4)))); val spans = segments - |> maps (Command_Span.content o #span) + |> maps segment_content |> drop_suffix Token.is_space |> Source.of_list |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))