# HG changeset patch # User paulson # Date 1672352065 0 # Node ID 8a17349143df036db561f28b5333ea46ce6f5c17 # Parent 947510ce4e36fce5d5f74cc8e2dd473661f672cc# Parent 25c0d4c0e1105cfeb42bc47b7c819ecde5fc4fc3 merged diff -r 25c0d4c0e110 -r 8a17349143df src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Thu Dec 29 22:14:12 2022 +0000 +++ b/src/Pure/Isar/outer_syntax.ML Thu Dec 29 22:14:25 2022 +0000 @@ -163,8 +163,7 @@ Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f))); val local_theory' = - local_theory_command - (fn a => fn b => fn c => Toplevel.local_theory' a b c Toplevel.no_presentation); + local_theory_command (fn a => fn b => fn c => Toplevel.local_theory' a b c NONE); val local_theory = local_theory_command Toplevel.local_theory; val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof'; val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof; diff -r 25c0d4c0e110 -r 8a17349143df src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Dec 29 22:14:12 2022 +0000 +++ b/src/Pure/Isar/toplevel.ML Thu Dec 29 22:14:25 2022 +0000 @@ -29,9 +29,7 @@ val pretty_state: state -> Pretty.T list val string_of_state: state -> string val pretty_abstract: state -> Pretty.T - type presentation = state -> Latex.text option - val presentation: (state -> Latex.text) -> presentation - val no_presentation: presentation + type presentation = state -> Latex.text type transition val empty: transition val name_of: transition -> string @@ -46,7 +44,7 @@ val is_init: transition -> bool val modify_init: (unit -> theory) -> transition -> transition val exit: transition -> transition - val present: (state -> Latex.text) -> transition -> transition + val present: presentation -> transition -> transition val keep: (state -> unit) -> transition -> transition val keep': (bool -> state -> unit) -> transition -> transition val keep_proof: (state -> unit) -> transition -> transition @@ -55,17 +53,17 @@ val ignored: Position.T -> transition val malformed: Position.T -> string -> transition val generic_theory: (generic_theory -> generic_theory) -> transition -> transition - val theory': (bool -> theory -> theory) -> presentation -> transition -> transition + val theory': (bool -> theory -> theory) -> presentation option -> transition -> transition val theory: (theory -> theory) -> transition -> transition val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition val end_main_target: transition -> transition val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition val end_nested_target: transition -> transition val local_theory': (bool * Position.T) option -> (xstring * Position.T) option -> - (bool -> local_theory -> local_theory) -> presentation -> transition -> transition + (bool -> local_theory -> local_theory) -> presentation option -> transition -> transition val local_theory: (bool * Position.T) option -> (xstring * Position.T) option -> (local_theory -> local_theory) -> transition -> transition - val present_local_theory: (xstring * Position.T) option -> (state -> Latex.text) -> + val present_local_theory: (xstring * Position.T) option -> presentation -> transition -> transition val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option -> (bool -> local_theory -> Proof.state) -> transition -> transition @@ -141,12 +139,12 @@ (node, cases_node init_presentation Context.proof_of Proof.context_of node); datatype state = - State of node_presentation * (theory option * Latex.text option); + State of node_presentation * (theory option * Latex.text future 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 output_of (State (_, (_, output))) = output; +fun output_of (State (_, (_, output))) = Option.map Future.join output; fun make_state opt_thy = let val node = (case opt_thy of NONE => Toplevel | SOME thy => Theory (Context.Theory thy)) @@ -256,14 +254,9 @@ (** toplevel transitions **) -(* presentation *) +(* primitive transitions *) -type presentation = state -> Latex.text option; -fun presentation g : presentation = SOME o g; -val no_presentation: presentation = K NONE; - - -(* primitive transitions *) +type presentation = state -> Latex.text; datatype trans = (*init theory*) @@ -271,78 +264,76 @@ (*formal exit of theory*) Exit | (*keep state unchanged*) - Keep of bool -> presentation | + Keep of (bool -> state -> unit) * presentation option | (*node transaction and presentation*) - Transaction of (bool -> node -> node_presentation) * presentation; + Transaction of (bool -> node -> node_presentation) * presentation option; local -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 = +fun present_state fork g node_pr prev_thy = let - val node_pr = node_presentation node; - val context = cases_proper_node I (Context.Proof o Proof.context_of) node; - fun make_state node_pr' = State (node_pr', (get_theory node, NONE)); + val state = State (node_pr, (prev_thy, NONE)); + fun present pr = + if fork andalso Future.proofs_enabled 1 then + Execution.fork {name = "Toplevel.present_state", pos = Position.thread_data (), pri = ~1} + (fn () => pr state) + else Future.value (pr state); + in State (node_pr, (prev_thy, Option.map present g)) end; - 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 => st' - | SOME exn => raise FAILURE (st', exn)) - end; +fun no_update f g state = + Runtime.controlled_execution (try generic_theory_of state) + (fn () => + let + val prev_thy = previous_theory_of state; + val () = f state; + val node_pr = node_presentation (node_of state); + in present_state false g node_pr prev_thy end) () + +fun update f g state = + Runtime.controlled_execution (try generic_theory_of state) + (fn () => + let + val prev_thy = previous_theory_of state; + val node_pr' = f (node_of state); + in present_state true g node_pr' prev_thy 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, NONE))) () - | (Exit, node as Theory (Context.Theory thy)) => + | (Exit, Theory (Context.Theory thy)) => let val State ((node', pr_ctxt), _) = - node |> apply + state |> update (fn _ => node_presentation (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy))))) - no_presentation; + NONE; in State ((Toplevel, pr_ctxt), (get_theory node', NONE)) end - | (Keep f, node) => - Runtime.controlled_execution (try generic_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) () + | (Keep (f, g), _) => no_update (fn x => f int x) g state | (Transaction _, Toplevel) => raise UNDEF - | (Transaction (f, g), node) => apply (fn x => f int x) g node + | (Transaction (f, g), _) => update (fn x => f int x) g state | _ => raise UNDEF); -fun apply_union _ [] state = raise FAILURE (state, UNDEF) - | apply_union int (tr :: trs) state = - apply_union int trs state - handle Runtime.UNDEF => apply_tr int tr state - | FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state - | exn as FAILURE _ => raise exn - | exn => raise FAILURE (state, exn); +fun apply_body _ [] _ = raise UNDEF + | apply_body int [tr] state = apply_tr int tr state + | apply_body int (tr :: trs) state = + apply_body int trs state + handle Runtime.UNDEF => apply_tr int tr state; fun apply_markers name markers (state as State ((node, pr_ctxt), prev_thy)) = let val state' = Runtime.controlled_execution (try generic_theory_of state) (fn () => State ((node, fold (Document_Marker.evaluate name) markers pr_ctxt), prev_thy)) (); - in (state', NONE) end - handle exn => (state, SOME exn); + in (state', NONE) end; in -fun apply_trans int name markers trans state = - (apply_union int trans state |> apply_markers name markers) - handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); +fun apply_capture int name markers trans state = + (apply_body int trans state |> apply_markers name markers) + handle exn => (state, SOME exn); end; @@ -412,12 +403,12 @@ val exit = add_trans Exit; fun present_transaction f g = add_trans (Transaction (f, g)); -fun transaction f = present_transaction f no_presentation; -fun transaction0 f = present_transaction (node_presentation oo f) no_presentation; +fun transaction f = present_transaction f NONE; +fun transaction0 f = present_transaction (node_presentation oo f) NONE; -fun present f = add_trans (Keep (K (presentation f))); -fun keep f = add_trans (Keep (fn _ => fn st => let val () = f st in NONE end)); -fun keep' f = add_trans (Keep (fn int => fn st => let val () = f int st in NONE end)); +fun present g = add_trans (Keep (fn _ => fn _ => (), SOME g)); +fun keep f = add_trans (Keep (K f, NONE)); +fun keep' f = add_trans (Keep (f, NONE)); fun keep_proof f = keep (fn st => @@ -453,7 +444,7 @@ in node_presentation (Theory (Context.Theory thy')) end | _ => raise UNDEF)); -fun theory f = theory' (K f) no_presentation; +fun theory f = theory' (K f) NONE; fun begin_main_target begin f = transaction (fn _ => (fn Theory (Context.Theory thy) => @@ -505,14 +496,14 @@ | _ => raise UNDEF)); fun local_theory restricted target f = - local_theory' restricted target (K f) no_presentation; + local_theory' restricted target (K f) NONE; fun present_local_theory target g = present_transaction (fn _ => (fn Theory gthy => let val (finish, lthy) = Target_Context.switch_named_cmd target gthy; in (Theory (finish lthy), lthy) end | _ => raise UNDEF)) - (presentation g); + (SOME g); (* proof transitions *) @@ -641,8 +632,8 @@ fun app int (tr as Transition {name, markers, trans, ...}) = setmp_thread_position tr - (Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans) - ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn) + (Timing.protocol (name_of tr) (pos_of tr) (apply_capture int name markers trans) + ##> Option.map (fn Runtime.UNDEF => ERROR (type_error tr) | exn => exn) #> show_state); in @@ -790,8 +781,7 @@ val future_proof = Proof.future_proof (fn state => - Execution.fork - {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1} + Execution.fork {name = "Toplevel.future_proof", pos = pos_of head_tr, pri = ~1} (fn () => let val State ((Proof (prf, (_, orig_gthy)), _), prev_thy) = st'; diff -r 25c0d4c0e110 -r 8a17349143df src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Thu Dec 29 22:14:12 2022 +0000 +++ b/src/Pure/PIDE/resources.ML Thu Dec 29 22:14:25 2022 +0000 @@ -38,6 +38,7 @@ {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T, imports: (string * Position.T) list, keywords: Thy_Header.keywords} val read_file_node: string -> Path.T -> Path.T * Position.T -> Token.file + val read_file: Path.T -> Path.T * Position.T -> Token.file val parsed_files: (Path.T -> Path.T list) -> Token.file Exn.result list * Input.source -> theory -> Token.file list val parse_files: (Path.T -> Path.T list) -> (theory -> Token.file list) parser @@ -330,7 +331,7 @@ end; -(* read_file_node *) +(* read_file *) fun read_file_node file_node master_dir (src_path, pos) = let @@ -358,6 +359,8 @@ in {src_path = src_path, lines = lines, digest = digest, pos = Position.copy_id pos file_pos} end handle ERROR msg => error (msg ^ Position.here pos); +val read_file = read_file_node ""; + (* load files *) @@ -374,7 +377,7 @@ [(pos, Markup.path (Path.implode_symbolic (master_dir + src_path))), (pos, Markup.language_path delimited)]); val _ = Position.reports reports; - in map (read_file_node "" master_dir o rpair pos) src_paths end + in map (read_file master_dir o rpair pos) src_paths end else map Exn.release files; fun parse_files make_paths =