simplified Toplevel.init_theory: discontinued special master argument;
authorwenzelm
Sat Aug 13 20:41:29 2011 +0200 (2011-08-13 ago)
changeset 44186806f0ec1a43d
parent 44185 05641edb5d30
child 44187 88d770052bac
simplified Toplevel.init_theory: discontinued special master argument;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Aug 13 20:20:36 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Aug 13 20:41:29 2011 +0200
     1.3 @@ -30,9 +30,10 @@
     1.4    Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
     1.5      (Thy_Header.args >> (fn (name, imports, uses) =>
     1.6        Toplevel.print o
     1.7 -        Toplevel.init_theory NONE name
     1.8 -          (fn master =>
     1.9 -            Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses))));
    1.10 +        Toplevel.init_theory name
    1.11 +          (fn () =>
    1.12 +            Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
    1.13 +              name imports (map (apfst Path.explode) uses))));
    1.14  
    1.15  val _ =
    1.16    Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 20:20:36 2011 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 20:41:29 2011 +0200
     2.3 @@ -35,7 +35,7 @@
     2.4    type isar
     2.5    val isar: TextIO.instream -> bool -> isar
     2.6    val prepare_span: outer_syntax -> Thy_Syntax.span -> Toplevel.transition * bool
     2.7 -  val prepare_element: outer_syntax -> (Path.T option -> theory) -> Thy_Syntax.element ->
     2.8 +  val prepare_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.element ->
     2.9      (Toplevel.transition * Toplevel.transition list) list
    2.10    val prepare_command: Position.T -> string -> Toplevel.transition
    2.11  end;
    2.12 @@ -224,7 +224,7 @@
    2.13  fun process_file path thy =
    2.14    let
    2.15      val trs = parse (Path.position path) (File.read path);
    2.16 -    val init = Toplevel.init_theory NONE "" (K thy) Toplevel.empty;
    2.17 +    val init = Toplevel.init_theory "" (K thy) Toplevel.empty;
    2.18      val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
    2.19    in
    2.20      (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
     3.1 --- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:20:36 2011 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:41:29 2011 +0200
     3.3 @@ -45,9 +45,8 @@
     3.4    val set_print: bool -> transition -> transition
     3.5    val print: transition -> transition
     3.6    val no_timing: transition -> transition
     3.7 -  val init_theory: Path.T option -> string -> (Path.T option -> theory) -> transition -> transition
     3.8 -  val modify_master: Path.T option -> transition -> transition
     3.9 -  val modify_init: (Path.T option -> theory) -> transition -> transition
    3.10 +  val init_theory: string -> (unit -> theory) -> transition -> transition
    3.11 +  val modify_init: (unit -> theory) -> transition -> transition
    3.12    val exit: transition -> transition
    3.13    val keep: (state -> unit) -> transition -> transition
    3.14    val keep': (bool -> state -> unit) -> transition -> transition
    3.15 @@ -297,16 +296,16 @@
    3.16  (* primitive transitions *)
    3.17  
    3.18  datatype trans =
    3.19 -  Init of Path.T option * string * (Path.T option -> theory) | (*master dir, theory name, init*)
    3.20 +  Init of string * (unit -> theory) | (*theory name, init*)
    3.21    Exit |                                 (*formal exit of theory*)
    3.22    Keep of bool -> state -> unit |        (*peek at state*)
    3.23    Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
    3.24  
    3.25  local
    3.26  
    3.27 -fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
    3.28 +fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
    3.29        State (SOME (Theory (Context.Theory
    3.30 -          (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
    3.31 +          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
    3.32    | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
    3.33        exit_transaction state
    3.34    | apply_tr int (Keep f) state =
    3.35 @@ -398,16 +397,11 @@
    3.36  
    3.37  (* basic transitions *)
    3.38  
    3.39 -fun init_theory master name f = add_trans (Init (master, name, f));
    3.40 -
    3.41 -fun modify_master master tr =
    3.42 -  (case get_init tr of
    3.43 -    SOME (_, name, f) => init_theory master name f (reset_trans tr)
    3.44 -  | NONE => tr);
    3.45 +fun init_theory name f = add_trans (Init (name, f));
    3.46  
    3.47  fun modify_init f tr =
    3.48    (case get_init tr of
    3.49 -    SOME (master, name, _) => init_theory master name f (reset_trans tr)
    3.50 +    SOME (name, _) => init_theory name f (reset_trans tr)
    3.51    | NONE => tr);
    3.52  
    3.53  val exit = add_trans Exit;
     4.1 --- a/src/Pure/PIDE/document.ML	Sat Aug 13 20:20:36 2011 +0200
     4.2 +++ b/src/Pure/PIDE/document.ML	Sat Aug 13 20:41:29 2011 +0200
     4.3 @@ -280,12 +280,12 @@
     4.4      val is_init = Toplevel.is_init raw_tr;
     4.5      val tr =
     4.6        if is_init then
     4.7 -        raw_tr |> Toplevel.modify_init (fn _ =>
     4.8 +        raw_tr |> Toplevel.modify_init (fn () =>
     4.9            let
    4.10              (* FIXME get theories from document state *)
    4.11              (* FIXME provide files via Scala layer *)
    4.12              val (name, imports, uses) = Exn.release node_header;
    4.13 -            val master = SOME (Path.dir (Path.explode node_name));
    4.14 +            val master = Path.dir (Path.explode node_name);
    4.15            in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end)
    4.16        else raw_tr;
    4.17  
     5.1 --- a/src/Pure/Thy/thy_info.ML	Sat Aug 13 20:20:36 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Aug 13 20:41:29 2011 +0200
     5.3 @@ -21,8 +21,7 @@
     5.4    val use_thys_wrt: Path.T -> string list -> unit
     5.5    val use_thys: string list -> unit
     5.6    val use_thy: string -> unit
     5.7 -  val toplevel_begin_theory: Path.T option -> string ->
     5.8 -    string list -> (Path.T * bool) list -> theory
     5.9 +  val toplevel_begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory
    5.10    val register_thy: theory -> unit
    5.11    val finish: unit -> unit
    5.12  end;
    5.13 @@ -312,9 +311,8 @@
    5.14  
    5.15  (* toplevel begin theory -- without maintaining database *)
    5.16  
    5.17 -fun toplevel_begin_theory master name imports uses =
    5.18 +fun toplevel_begin_theory dir name imports uses =
    5.19    let
    5.20 -    val dir = (case master of SOME dir => dir | NONE => Thy_Load.get_master_path ());
    5.21      val _ = kill_thy name;
    5.22      val _ = use_thys_wrt dir imports;
    5.23      val parents = map (get_theory o base_name) imports;
     6.1 --- a/src/Pure/Thy/thy_load.ML	Sat Aug 13 20:20:36 2011 +0200
     6.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Aug 13 20:41:29 2011 +0200
     6.3 @@ -167,7 +167,7 @@
     6.4      val time = ! Toplevel.timing;
     6.5  
     6.6      val _ = Present.init_theory name;
     6.7 -    fun init _ =
     6.8 +    fun init () =
     6.9        begin_theory dir name imports uses parents
    6.10        |> Present.begin_theory update_time dir uses;
    6.11