tuned signature;
authorwenzelm
Fri Mar 08 19:22:28 2019 +0100 (3 months ago ago)
changeset 7005845b2e784350a
parent 70057 b49bd228ac8a
child 70059 ccc8e4c99520
tuned signature;
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Mar 08 17:05:23 2019 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Mar 08 19:22:28 2019 +0100
     1.3 @@ -33,9 +33,11 @@
     1.4    val empty: transition
     1.5    val name_of: transition -> string
     1.6    val pos_of: transition -> Position.T
     1.7 +  val timing_of: transition -> Time.time
     1.8    val type_error: transition -> string
     1.9    val name: string -> transition -> transition
    1.10    val position: Position.T -> transition -> transition
    1.11 +  val timing: Time.time -> transition -> transition
    1.12    val init_theory: (unit -> theory) -> transition -> transition
    1.13    val is_init: transition -> bool
    1.14    val modify_init: (unit -> theory) -> transition -> transition
    1.15 @@ -77,8 +79,6 @@
    1.16    val exec_id: Document_ID.exec -> transition -> transition
    1.17    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
    1.18    val add_hook: (transition -> state -> state -> unit) -> unit
    1.19 -  val get_timing: transition -> Time.time
    1.20 -  val put_timing: Time.time -> transition -> transition
    1.21    val transition: bool -> transition -> state -> state * (exn * string) option
    1.22    val command_errors: bool -> transition -> state -> Runtime.error list * state option
    1.23    val command_exception: bool -> transition -> state -> state
    1.24 @@ -327,6 +327,7 @@
    1.25  
    1.26  fun name_of (Transition {name, ...}) = name;
    1.27  fun pos_of (Transition {pos, ...}) = pos;
    1.28 +fun timing_of (Transition {timing, ...}) = timing;
    1.29  
    1.30  fun command_msg msg tr =
    1.31    msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^
    1.32 @@ -344,6 +345,9 @@
    1.33  fun position pos = map_transition (fn (name, _, timing, trans) =>
    1.34    (name, pos, timing, trans));
    1.35  
    1.36 +fun timing timing = map_transition (fn (name, pos, _, trans) =>
    1.37 +  (name, pos, timing, trans));
    1.38 +
    1.39  fun add_trans tr = map_transition (fn (name, pos, timing, trans) =>
    1.40    (name, pos, timing, tr :: trans));
    1.41  
    1.42 @@ -582,9 +586,6 @@
    1.43  
    1.44  (* apply transitions *)
    1.45  
    1.46 -fun get_timing (Transition {timing, ...}) = timing;
    1.47 -fun put_timing timing = map_transition (fn (name, pos, _, trans) => (name, pos, timing, trans));
    1.48 -
    1.49  local
    1.50  
    1.51  fun app int (tr as Transition {trans, ...}) =
    1.52 @@ -678,7 +679,7 @@
    1.53  
    1.54  fun timing_estimate elem =
    1.55    let val trs = tl (Thy_Element.flat_element elem)
    1.56 -  in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
    1.57 +  in fold (fn tr => fn t => timing_of tr + t) trs Time.zeroTime end;
    1.58  
    1.59  fun future_proofs_enabled estimate st =
    1.60    (case try proof_of st of
     2.1 --- a/src/Pure/Thy/thy_info.ML	Fri Mar 08 17:05:23 2019 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Mar 08 19:22:28 2019 +0100
     2.3 @@ -285,7 +285,7 @@
     2.4      fun prepare_span st span =
     2.5        Command_Span.content span
     2.6        |> Command.read keywords (Command.read_thy st) master_dir init ([], ~1)
     2.7 -      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
     2.8 +      |> (fn tr => Toplevel.timing (last_timing tr) tr);
     2.9  
    2.10      fun element_result span_elem (st, _) =
    2.11        let