simplified Toplevel.init_theory: discontinued special name argument;
authorwenzelm
Sat Aug 13 20:49:41 2011 +0200 (2011-08-13 ago)
changeset 4418788d770052bac
parent 44186 806f0ec1a43d
child 44188 9e6698b9dcea
simplified Toplevel.init_theory: discontinued special name argument;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Aug 13 20:41:29 2011 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Aug 13 20:49:41 2011 +0200
     1.3 @@ -30,7 +30,7 @@
     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 name
     1.8 +        Toplevel.init_theory
     1.9            (fn () =>
    1.10              Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ())
    1.11                name imports (map (apfst Path.explode) uses))));
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 20:41:29 2011 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Aug 13 20:49:41 2011 +0200
     2.3 @@ -224,7 +224,7 @@
     2.4  fun process_file path thy =
     2.5    let
     2.6      val trs = parse (Path.position path) (File.read path);
     2.7 -    val init = Toplevel.init_theory "" (K thy) Toplevel.empty;
     2.8 +    val init = Toplevel.init_theory (K thy) Toplevel.empty;
     2.9      val result = fold Toplevel.command (init :: trs) Toplevel.toplevel;
    2.10    in
    2.11      (case (Toplevel.is_theory result, Toplevel.generic_theory_of result) of
     3.1 --- a/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:41:29 2011 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Aug 13 20:49:41 2011 +0200
     3.3 @@ -34,7 +34,6 @@
     3.4    val thread: bool -> (unit -> unit) -> Thread.thread
     3.5    type transition
     3.6    val empty: transition
     3.7 -  val is_init: transition -> bool
     3.8    val print_of: transition -> bool
     3.9    val name_of: transition -> string
    3.10    val pos_of: transition -> Position.T
    3.11 @@ -45,7 +44,8 @@
    3.12    val set_print: bool -> transition -> transition
    3.13    val print: transition -> transition
    3.14    val no_timing: transition -> transition
    3.15 -  val init_theory: string -> (unit -> theory) -> transition -> transition
    3.16 +  val init_theory: (unit -> theory) -> transition -> transition
    3.17 +  val is_init: transition -> bool
    3.18    val modify_init: (unit -> theory) -> transition -> transition
    3.19    val exit: transition -> transition
    3.20    val keep: (state -> unit) -> transition -> transition
    3.21 @@ -296,14 +296,14 @@
    3.22  (* primitive transitions *)
    3.23  
    3.24  datatype trans =
    3.25 -  Init of string * (unit -> theory) | (*theory name, init*)
    3.26 +  Init of unit -> theory |               (*init theory*)
    3.27    Exit |                                 (*formal exit of theory*)
    3.28    Keep of bool -> state -> unit |        (*peek at state*)
    3.29    Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
    3.30  
    3.31  local
    3.32  
    3.33 -fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
    3.34 +fun apply_tr _ (Init f) (State (NONE, _)) =
    3.35        State (SOME (Theory (Context.Theory
    3.36            (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
    3.37    | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
    3.38 @@ -352,11 +352,6 @@
    3.39  
    3.40  (* diagnostics *)
    3.41  
    3.42 -fun get_init (Transition {trans = [Init args], ...}) = SOME args
    3.43 -  | get_init _ = NONE;
    3.44 -
    3.45 -val is_init = is_some o get_init;
    3.46 -
    3.47  fun print_of (Transition {print, ...}) = print;
    3.48  fun name_of (Transition {name, ...}) = name;
    3.49  fun pos_of (Transition {pos, ...}) = pos;
    3.50 @@ -397,12 +392,12 @@
    3.51  
    3.52  (* basic transitions *)
    3.53  
    3.54 -fun init_theory name f = add_trans (Init (name, f));
    3.55 +fun init_theory f = add_trans (Init f);
    3.56  
    3.57 -fun modify_init f tr =
    3.58 -  (case get_init tr of
    3.59 -    SOME (name, _) => init_theory name f (reset_trans tr)
    3.60 -  | NONE => tr);
    3.61 +fun is_init (Transition {trans = [Init _], ...}) = true
    3.62 +  | is_init _ = false;
    3.63 +
    3.64 +fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr;
    3.65  
    3.66  val exit = add_trans Exit;
    3.67  val keep' = add_trans o Keep;