# HG changeset patch # User wenzelm # Date 1280061708 -7200 # Node ID ddc3b72f9a4295697f4236a5d1a63a197694f3f9 # Parent f6c40213675b2ca90f04c9031d672118c1c760e5 simplified handling of theory begin/end wrt. toplevel and theory loader; diff -r f6c40213675b -r ddc3b72f9a42 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sun Jul 25 12:57:29 2010 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sun Jul 25 14:41:48 2010 +0200 @@ -275,8 +275,7 @@ fun init_theory (name, imports, uses) = Toplevel.init_theory name - (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses)) - (Theory.end_theory #> Thy_Info.end_theory); + (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses)); val exit = Toplevel.keep (fn state => (Context.set_thread_data (try Toplevel.generic_theory_of state); diff -r f6c40213675b -r ddc3b72f9a42 src/Pure/Isar/isar_document.ML --- a/src/Pure/Isar/isar_document.ML Sun Jul 25 12:57:29 2010 +0200 +++ b/src/Pure/Isar/isar_document.ML Sun Jul 25 14:41:48 2010 +0200 @@ -192,13 +192,10 @@ val end_state = the_state (the (#state (#3 (the (first_entry (fn (_, {next, ...}) => is_none next) document))))); - val _ = (* FIXME regular execution (??) *) + val _ = (* FIXME regular execution (??), result (??) *) Future.fork (fn () => (case Lazy.force end_state of - SOME st => - (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st; - Thy_Info.touch_child_thys name; - Thy_Info.register_thy name) + SOME st => Toplevel.end_theory (Position.id_only id) st | NONE => error ("Failed to finish theory " ^ quote name))); in () end); diff -r f6c40213675b -r ddc3b72f9a42 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sun Jul 25 12:57:29 2010 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Sun Jul 25 14:41:48 2010 +0200 @@ -31,7 +31,7 @@ type isar val isar: bool -> isar val prepare_command: Position.T -> string -> Toplevel.transition - val load_thy: string -> Position.T -> string -> unit -> unit + val load_thy: string -> Position.T -> string -> (unit -> unit) * theory end; structure Outer_Syntax: OUTER_SYNTAX = @@ -204,7 +204,7 @@ fun process_file path thy = let val trs = parse (Path.position path) (File.read path); - val init = Toplevel.init_theory "" (K thy) (K ()) Toplevel.empty; + val init = Toplevel.init_theory "" (K thy) Toplevel.empty; val result = fold Toplevel.command (init :: trs) Toplevel.toplevel; in (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of @@ -285,14 +285,14 @@ (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans); val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else (); - val results = cond_timeit time "" (fn () => Toplevel.excursion units); + val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion units); val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else (); fun after_load () = Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks |> Buffer.content |> Present.theory_output name; - in after_load end; + in (after_load, thy) end; end; diff -r f6c40213675b -r ddc3b72f9a42 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sun Jul 25 12:57:29 2010 +0200 +++ b/src/Pure/Isar/toplevel.ML Sun Jul 25 14:41:48 2010 +0200 @@ -21,6 +21,7 @@ val proof_of: state -> Proof.state val proof_position_of: state -> int val enter_proof_body: state -> Proof.state + val end_theory: Position.T -> state -> theory val print_state_context: state -> unit val print_state: bool -> state -> unit val pretty_abstract: state -> Pretty.T @@ -45,7 +46,7 @@ val interactive: bool -> transition -> transition val print: transition -> transition val no_timing: transition -> transition - val init_theory: string -> (bool -> theory) -> (theory -> unit) -> transition -> transition + val init_theory: string -> (bool -> theory) -> transition -> transition val exit: transition -> transition val keep: (state -> unit) -> transition -> transition val keep': (bool -> state -> unit) -> transition -> transition @@ -87,9 +88,8 @@ val add_hook: (transition -> state -> state -> unit) -> unit val transition: bool -> transition -> state -> (state * (exn * string) option) option val run_command: string -> transition -> state -> state option - val commit_exit: Position.T -> transition val command: transition -> state -> state - val excursion: (transition * transition list) list -> (transition * state) list lazy + val excursion: (transition * transition list) list -> (transition * state) list lazy * theory end; structure Toplevel: TOPLEVEL = @@ -137,8 +137,7 @@ (* datatype state *) -type node_info = node * (theory -> unit); (*node with exit operation*) -datatype state = State of node_info option * node_info option; (*current, previous*) +datatype state = State of node option * node option; (*current, previous*) val toplevel = State (NONE, NONE); @@ -146,21 +145,21 @@ | is_toplevel _ = false; fun level (State (NONE, _)) = 0 - | level (State (SOME (Theory _, _), _)) = 0 - | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf) - | level (State (SOME (SkipProof (d, _), _), _)) = d + 1; (*different notion of proof depth!*) + | level (State (SOME (Theory _), _)) = 0 + | level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf) + | level (State (SOME (SkipProof (d, _)), _)) = d + 1; (*different notion of proof depth!*) fun str_of_state (State (NONE, _)) = "at top level" - | str_of_state (State (SOME (Theory (Context.Theory _, _), _), _)) = "in theory mode" - | str_of_state (State (SOME (Theory (Context.Proof _, _), _), _)) = "in local theory mode" - | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode" - | str_of_state (State (SOME (SkipProof _, _), _)) = "in skipped proof mode"; + | str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode" + | str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode" + | str_of_state (State (SOME (Proof _), _)) = "in proof mode" + | str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode"; (* current node *) fun node_of (State (NONE, _)) = raise UNDEF - | node_of (State (SOME (node, _), _)) = node; + | node_of (State (SOME node, _)) = node; fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); @@ -174,7 +173,7 @@ | NONE => raise UNDEF); fun previous_context_of (State (_, NONE)) = NONE - | previous_context_of (State (_, SOME (prev, _))) = SOME (context_node prev); + | previous_context_of (State (_, SOME prev)) = SOME (context_node prev); val context_of = node_case Context.proof_of Proof.context_of; val generic_theory_of = node_case I (Context.Proof o Proof.context_of); @@ -188,6 +187,9 @@ val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward; +fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy + | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos); + (* print state *) @@ -264,12 +266,12 @@ in -fun apply_transaction f g (node, exit) = +fun apply_transaction f g node = let val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state"; val cont_node = reset_presentation node; val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node; - fun state_error e nd = (State (SOME (nd, exit), SOME (node, exit)), e); + fun state_error e nd = (State (SOME nd, SOME node), e); val (result, err) = cont_node @@ -293,21 +295,18 @@ (* primitive transitions *) datatype trans = - Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*) - Exit | (*formal exit of theory -- without committing*) - Commit_Exit | (*exit and commit final theory*) - Keep of bool -> state -> unit | (*peek at state*) + Init of string * (bool -> theory) | (*theory name, init*) + Exit | (*formal exit of theory*) + Keep of bool -> state -> unit | (*peek at state*) Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*) local -fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) = +fun apply_tr int (Init (_, f)) (State (NONE, _)) = State (SOME (Theory (Context.Theory - (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE) - | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) = + (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE) + | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) = State (NONE, prev) - | apply_tr _ Commit_Exit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) = - (Runtime.controlled_execution exit thy; toplevel) | apply_tr int (Keep f) state = Runtime.controlled_execution (fn x => tap (f int) x) state | apply_tr int (Transaction (f, g)) (State (SOME state, _)) = @@ -352,7 +351,7 @@ (* diagnostics *) -fun init_of (Transition {trans = [Init (name, _, _)], ...}) = SOME name +fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name | init_of _ = NONE; fun name_of (Transition {name, ...}) = name; @@ -394,7 +393,7 @@ (* basic transitions *) -fun init_theory name f exit = add_trans (Init (name, f, exit)); +fun init_theory name f = add_trans (Init (name, f)); val exit = add_trans Exit; val keep' = add_trans o Keep; @@ -643,15 +642,6 @@ | Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE)); -(* commit final exit *) - -fun commit_exit pos = - name "end" empty - |> position pos - |> add_trans Commit_Exit - |> imperative (fn () => warning "Expected to find finished theory"); - - (* nested commands *) fun command tr st = @@ -693,8 +683,8 @@ (fn prf => Future.fork_pri ~1 (fn () => let val (states, result_state) = - (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev) - => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev)) + (case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) + => State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) |> fold_map command_result body_trs ||> command (end_tr |> set_print false); in (states, presentation_context_of result_state) end)) @@ -715,14 +705,9 @@ fun excursion input = let val end_pos = if null input then error "No input" else pos_of (fst (List.last input)); - val immediate = not (Goal.future_enabled ()); val (results, end_state) = fold_map (proof_result immediate) input toplevel; - val _ = - (case end_state of - State (NONE, SOME (Theory (Context.Theory _, _), _)) => - command (commit_exit end_pos) end_state - | _ => error "Unfinished development at end of input"); - in Lazy.lazy (fn () => maps Lazy.force results) end; + val thy = end_theory end_pos end_state; + in (Lazy.lazy (fn () => maps Lazy.force results), thy) end; end; diff -r f6c40213675b -r ddc3b72f9a42 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Jul 25 12:57:29 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sun Jul 25 14:41:48 2010 +0200 @@ -138,8 +138,8 @@ val _ = name = "" andalso error ("Bad file name: " ^ quote file); val _ = if Thy_Info.known_thy name then - (Isar.>> (Toplevel.commit_exit Position.none); - Thy_Info.touch_child_thys name; Thy_Info.register_thy name) + (Thy_Info.register_thy name (Toplevel.end_theory Position.none (Isar.state ())); + Thy_Info.touch_child_thys name) handle ERROR msg => (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]); tell_file_retracted (Thy_Header.thy_path name)) diff -r f6c40213675b -r ddc3b72f9a42 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Jul 25 12:57:29 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Jul 25 14:41:48 2010 +0200 @@ -224,7 +224,7 @@ let val name = thy_name path in if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then (Thy_Info.touch_child_thys name; - Thy_Info.register_thy name handle ERROR msg => + Thy_Info.register_thy name (Toplevel.end_theory Position.none state) handle ERROR msg => (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]); tell_file_retracted true (Path.base path))) else raise Toplevel.UNDEF diff -r f6c40213675b -r ddc3b72f9a42 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Jul 25 12:57:29 2010 +0200 +++ b/src/Pure/Thy/thy_info.ML Sun Jul 25 14:41:48 2010 +0200 @@ -25,8 +25,7 @@ val use_thys: string list -> unit val use_thy: string -> unit val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory - val end_theory: theory -> unit - val register_thy: string -> unit + val register_thy: string -> theory -> unit val register_theory: theory -> unit val finish: unit -> unit end; @@ -131,6 +130,7 @@ val lookup_deps = Option.map #1 o lookup_thy; val get_deps = #1 o get_thy; fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x)); +fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory)); val is_finished = is_none o get_deps; val master_directory = master_dir' o get_deps; @@ -255,10 +255,11 @@ else (Path.position master_path, text) | _ => corrupted ()); val _ = touch_thy name; - val _ = CRITICAL (fn () => + val _ = change_deps name (Option.map (fn {master, text, parents, ...} => - make_deps upd_time master text parents))); - val after_load = Outer_Syntax.load_thy name pos text; + make_deps upd_time master text parents)); + val (after_load, theory) = Outer_Syntax.load_thy name pos text; + val _ = put_theory name theory; val _ = CRITICAL (fn () => (change_deps name @@ -415,7 +416,7 @@ val use_thy = use_thys o single; -(* begin / end theory *) +(* begin theory *) fun check_unfinished name = if known_thy name andalso is_finished name then @@ -450,26 +451,22 @@ fold (fn x => Context.theory_map (Thy_Load.exec_ml x) o Theory.checkpoint) uses_now theory'; in theory'' end; -fun end_theory theory = - let val name = Context.theory_name theory - in if known_thy name then change_thy name (fn (deps, _) => (deps, SOME theory)) else () end; - (* register existing theories *) -fun register_thy name = +fun register_thy name theory = let val _ = priority ("Registering theory " ^ quote name); - val thy = get_theory name; val _ = map get_theory (get_parents name); val _ = check_unfinished name; val _ = touch_thy name; val master = #master (Thy_Load.deps_thy Path.current name); - val upd_time = #2 (Management_Data.get thy); + val upd_time = #2 (Management_Data.get theory); in CRITICAL (fn () => (change_deps name (Option.map (fn {parents, ...} => make_deps upd_time (SOME master) "" parents)); + put_theory name theory; perform Update name)) end;