eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
authorwenzelm
Wed Jul 21 16:14:16 2010 +0200 (2010-07-21 ago)
changeset 3787366d90b2b87bc
parent 37872 d83659570337
child 37874 954dc0c580bd
eliminated old time_use/time_use_thy variants -- timing is implicitly controlled via Output.timing;
misc tuning and simplification;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Thy/thy_info.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jul 21 15:44:36 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 21 16:14:16 2010 +0200
     1.3 @@ -314,7 +314,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
     1.6      (Parse.path >>
     1.7 -      (fn path => Toplevel.generic_theory (Thy_Info.exec_file false path #> propagate_env)));
     1.8 +      (fn path => Toplevel.generic_theory (Thy_Info.exec_file path #> propagate_env)));
     1.9  
    1.10  val _ =
    1.11    Outer_Syntax.command "ML" "ML text within theory or local theory"
     2.1 --- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 21 15:44:36 2010 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 21 16:14:16 2010 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4    type isar
     2.5    val isar: bool -> isar
     2.6    val prepare_command: Position.T -> string -> Toplevel.transition
     2.7 -  val load_thy: string -> Position.T -> string list -> bool -> unit -> unit
     2.8 +  val load_thy: string -> Position.T -> string list -> unit -> unit
     2.9  end;
    2.10  
    2.11  structure Outer_Syntax: OUTER_SYNTAX =
    2.12 @@ -268,9 +268,10 @@
    2.13  
    2.14  (* load_thy *)
    2.15  
    2.16 -fun load_thy name pos text time =
    2.17 +fun load_thy name pos text =
    2.18    let
    2.19      val (lexs, commands) = get_syntax ();
    2.20 +    val time = ! Output.timing;
    2.21  
    2.22      val _ = Present.init_theory name;
    2.23  
     3.1 --- a/src/Pure/Thy/thy_info.ML	Wed Jul 21 15:44:36 2010 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Jul 21 16:14:16 2010 +0200
     3.3 @@ -26,13 +26,11 @@
     3.4    val remove_thy: string -> unit
     3.5    val kill_thy: string -> unit
     3.6    val provide_file: Path.T -> string -> unit
     3.7 -  val load_file: bool -> Path.T -> unit
     3.8 -  val exec_file: bool -> Path.T -> Context.generic -> Context.generic
     3.9 +  val load_file: Path.T -> unit
    3.10 +  val exec_file: Path.T -> Context.generic -> Context.generic
    3.11    val use: string -> unit
    3.12 -  val time_use: string -> unit
    3.13    val use_thys: string list -> unit
    3.14    val use_thy: string -> unit
    3.15 -  val time_use_thy: string -> unit
    3.16    val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
    3.17    val end_theory: theory -> unit
    3.18    val register_thy: string -> unit
    3.19 @@ -306,8 +304,8 @@
    3.20      | NONE => error ("Could not find file " ^ quote (Path.implode path)))
    3.21    end;
    3.22  
    3.23 -fun load_file time path =
    3.24 -  if time then
    3.25 +fun load_file path =
    3.26 +  if ! Output.timing then
    3.27      let val name = Path.implode path in
    3.28        timeit (fn () =>
    3.29         (priority ("\n**** Starting file " ^ quote name ^ " ****");
    3.30 @@ -316,10 +314,9 @@
    3.31      end
    3.32    else run_file path;
    3.33  
    3.34 -fun exec_file time path = ML_Context.exec (fn () => load_file time path);
    3.35 +fun exec_file path = ML_Context.exec (fn () => load_file path);
    3.36  
    3.37 -val use = load_file false o Path.explode;
    3.38 -val time_use = load_file true o Path.explode;
    3.39 +val use = load_file o Path.explode;
    3.40  
    3.41  end;
    3.42  
    3.43 @@ -329,7 +326,7 @@
    3.44  fun required_by _ [] = ""
    3.45    | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
    3.46  
    3.47 -fun load_thy time upd_time initiators name =
    3.48 +fun load_thy upd_time initiators name =
    3.49    let
    3.50      val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
    3.51      val (pos, text, _) =
    3.52 @@ -341,7 +338,7 @@
    3.53      val _ = CRITICAL (fn () =>
    3.54        change_deps name (Option.map (fn {master, text, parents, files, ...} =>
    3.55          make_deps upd_time master text parents files)));
    3.56 -    val after_load = Outer_Syntax.load_thy name pos text (time orelse ! Output.timing);
    3.57 +    val after_load = Outer_Syntax.load_thy name pos text;
    3.58      val _ =
    3.59        CRITICAL (fn () =>
    3.60         (change_deps name
    3.61 @@ -458,9 +455,9 @@
    3.62  
    3.63  in
    3.64  
    3.65 -fun require_thys time initiators dir strs tasks =
    3.66 -      fold_map (require_thy time initiators dir) strs tasks |>> forall I
    3.67 -and require_thy time initiators dir str tasks =
    3.68 +fun require_thys initiators dir strs tasks =
    3.69 +      fold_map (require_thy initiators dir) strs tasks |>> forall I
    3.70 +and require_thy initiators dir str tasks =
    3.71    let
    3.72      val path = Path.expand (Path.explode str);
    3.73      val name = Path.implode (Path.base path);
    3.74 @@ -478,8 +475,7 @@
    3.75            val parent_names = map base_name parents;
    3.76  
    3.77            val (parents_current, tasks_graph') =
    3.78 -            require_thys time (name :: initiators)
    3.79 -              (Path.append dir (master_dir' deps)) parents tasks;
    3.80 +            require_thys (name :: initiators) (Path.append dir (master_dir' deps)) parents tasks;
    3.81  
    3.82            val all_current = current andalso parents_current;
    3.83            val _ = if not all_current andalso known_thy name then outdate_thy name else ();
    3.84 @@ -491,7 +487,7 @@
    3.85            val upd_time = serial ();
    3.86            val tasks_graph'' = tasks_graph' |> new_deps name parent_names
    3.87             (if all_current then Finished
    3.88 -            else Task (fn () => load_thy time upd_time initiators name));
    3.89 +            else Task (fn () => load_thy upd_time initiators name));
    3.90          in (all_current, tasks_graph'') end)
    3.91    end;
    3.92  
    3.93 @@ -500,25 +496,16 @@
    3.94  
    3.95  (* use_thy etc. *)
    3.96  
    3.97 -local
    3.98 +fun use_thys_dir dir arg =
    3.99 +  schedule_tasks (snd (require_thys [] dir arg Graph.empty));
   3.100  
   3.101 -fun gen_use_thy' req dir arg =
   3.102 -  schedule_tasks (snd (req [] dir arg Graph.empty));
   3.103 +val use_thys = use_thys_dir Path.current;
   3.104  
   3.105 -fun gen_use_thy req str =
   3.106 -  let val name = base_name str in
   3.107 -    check_unfinished warning name;
   3.108 -    gen_use_thy' req Path.current str
   3.109 -  end;
   3.110 -
   3.111 -in
   3.112 -
   3.113 -val use_thys_dir = gen_use_thy' (require_thys false);
   3.114 -val use_thys = use_thys_dir Path.current;
   3.115 -val use_thy = gen_use_thy (require_thy false);
   3.116 -val time_use_thy = gen_use_thy (require_thy true);
   3.117 -
   3.118 -end;
   3.119 +fun use_thy str =
   3.120 +  let
   3.121 +    val name = base_name str;
   3.122 +    val _ = check_unfinished warning name;
   3.123 +  in use_thys [str] end;
   3.124  
   3.125  
   3.126  (* begin / end theory *)
   3.127 @@ -545,7 +532,7 @@
   3.128  
   3.129      val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
   3.130      val theory'' =
   3.131 -      fold (fn x => Context.theory_map (exec_file false x) o Theory.checkpoint) uses_now theory';
   3.132 +      fold (fn x => Context.theory_map (exec_file x) o Theory.checkpoint) uses_now theory';
   3.133    in theory'' end;
   3.134  
   3.135  fun end_theory theory =
     4.1 --- a/src/Pure/pure_setup.ML	Wed Jul 21 15:44:36 2010 +0200
     4.2 +++ b/src/Pure/pure_setup.ML	Wed Jul 21 16:14:16 2010 +0200
     4.3 @@ -54,8 +54,6 @@
     4.4  fun use name = Toplevel.program (fn () => Thy_Info.use name);
     4.5  fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
     4.6  fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
     4.7 -fun time_use name = Toplevel.program (fn () => Thy_Info.time_use name);
     4.8 -fun time_use_thy name = Toplevel.program (fn () => Thy_Info.time_use_thy name);
     4.9  
    4.10  
    4.11  (* misc *)