# HG changeset patch
# User wenzelm
# Date 1313260889 -7200
# Node ID 806f0ec1a43dbc086763965aeca01635ca97c312
# Parent  05641edb5d308ff1e80d0c16540d1d87b8965e37
simplified Toplevel.init_theory: discontinued special master argument;

diff -r 05641edb5d30 -r 806f0ec1a43d src/Pure/Isar/isar_syn.ML
--- 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)
diff -r 05641edb5d30 -r 806f0ec1a43d src/Pure/Isar/outer_syntax.ML
--- 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
diff -r 05641edb5d30 -r 806f0ec1a43d src/Pure/Isar/toplevel.ML
--- 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;
diff -r 05641edb5d30 -r 806f0ec1a43d src/Pure/PIDE/document.ML
--- 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;
 
diff -r 05641edb5d30 -r 806f0ec1a43d src/Pure/Thy/thy_info.ML
--- 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;
diff -r 05641edb5d30 -r 806f0ec1a43d src/Pure/Thy/thy_load.ML
--- 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;