--- a/src/Pure/Isar/isar_syn.ML Sat Aug 13 20:20:36 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sat Aug 13 20:41:29 2011 +0200
@@ -30,9 +30,10 @@
Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
(Thy_Header.args >> (fn (name, imports, uses) =>
Toplevel.print o
- Toplevel.init_theory NONE name
- (fn master =>
- Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses))));
+ Toplevel.init_theory name
+ (fn () =>
+ Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
+ name imports (map (apfst Path.explode) uses))));
val _ =
Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
--- a/src/Pure/Isar/outer_syntax.ML Sat Aug 13 20:20:36 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Sat Aug 13 20:41:29 2011 +0200
@@ -35,7 +35,7 @@
type isar
val isar: TextIO.instream -> bool -> isar
val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
- val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element ->
+ val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
(Toplevel.transition * Toplevel.transition list) list
val prepare_command: Position.T -> string -> Toplevel.transition
end;
@@ -224,7 +224,7 @@
fun process_file path thy =
let
val trs = parse (Path.position path) (File.read path);
- val init = Toplevel.init_theory NONE "" (K thy) 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
--- a/src/Pure/Isar/toplevel.ML Sat Aug 13 20:20:36 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat Aug 13 20:41:29 2011 +0200
@@ -45,9 +45,8 @@
val set_print: bool -> transition -> transition
val print: transition -> transition
val no_timing: transition -> transition
- val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
- val modify_master: Path.T option -> transition -> transition
- val modify_init: (Path.T option -> theory) -> transition -> transition
+ val init_theory: string -> (unit -> theory) -> transition -> transition
+ val modify_init: (unit -> theory) -> transition -> transition
val exit: transition -> transition
val keep: (state -> unit) -> transition -> transition
val keep': (bool -> state -> unit) -> transition -> transition
@@ -297,16 +296,16 @@
(* primitive transitions *)
datatype trans =
- Init of Path.T option * string * (Path.T option -> theory) | (*master dir, theory name, init*)
+ Init of string * (unit -> 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 _ (Init (master, _, f)) (State (NONE, _)) =
+fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
State (SOME (Theory (Context.Theory
- (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
+ (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
| apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
exit_transaction state
| apply_tr int (Keep f) state =
@@ -398,16 +397,11 @@
(* basic transitions *)
-fun init_theory master name f = add_trans (Init (master, name, f));
-
-fun modify_master master tr =
- (case get_init tr of
- SOME (_, name, f) => init_theory master name f (reset_trans tr)
- | NONE => tr);
+fun init_theory name f = add_trans (Init (name, f));
fun modify_init f tr =
(case get_init tr of
- SOME (master, name, _) => init_theory master name f (reset_trans tr)
+ SOME (name, _) => init_theory name f (reset_trans tr)
| NONE => tr);
val exit = add_trans Exit;
--- a/src/Pure/PIDE/document.ML Sat Aug 13 20:20:36 2011 +0200
+++ b/src/Pure/PIDE/document.ML Sat Aug 13 20:41:29 2011 +0200
@@ -280,12 +280,12 @@
val is_init = Toplevel.is_init raw_tr;
val tr =
if is_init then
- raw_tr |> Toplevel.modify_init (fn _ =>
+ raw_tr |> Toplevel.modify_init (fn () =>
let
(* FIXME get theories from document state *)
(* FIXME provide files via Scala layer *)
val (name, imports, uses) = Exn.release node_header;
- val master = SOME (Path.dir (Path.explode node_name));
+ val master = Path.dir (Path.explode node_name);
in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end)
else raw_tr;
--- a/src/Pure/Thy/thy_info.ML Sat Aug 13 20:20:36 2011 +0200
+++ b/src/Pure/Thy/thy_info.ML Sat Aug 13 20:41:29 2011 +0200
@@ -21,8 +21,7 @@
val use_thys_wrt: Path.T -> string list -> unit
val use_thys: string list -> unit
val use_thy: string -> unit
- val toplevel_begin_theory: Path.T option -> string ->
- string list -> (Path.T * bool) list -> theory
+ val toplevel_begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory
val register_thy: theory -> unit
val finish: unit -> unit
end;
@@ -312,9 +311,8 @@
(* toplevel begin theory -- without maintaining database *)
-fun toplevel_begin_theory master name imports uses =
+fun toplevel_begin_theory dir name imports uses =
let
- val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
val _ = kill_thy name;
val _ = use_thys_wrt dir imports;
val parents = map (get_theory o base_name) imports;
--- a/src/Pure/Thy/thy_load.ML Sat Aug 13 20:20:36 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML Sat Aug 13 20:41:29 2011 +0200
@@ -167,7 +167,7 @@
val time = ! Toplevel.timing;
val _ = Present.init_theory name;
- fun init _ =
+ fun init () =
begin_theory dir name imports uses parents
|> Present.begin_theory update_time dir uses;