src/Pure/PIDE/document.ML
changeset 47628 3275758d274e
parent 47424 57ff63a52c53
child 47630 8d654975b67d
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Apr 20 15:49:45 2012 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Apr 20 20:21:22 2012 +0200
     1.3 @@ -29,6 +29,7 @@
     1.4    val discontinue_execution: state -> unit
     1.5    val cancel_execution: state -> unit
     1.6    val start_execution: state -> unit
     1.7 +  val timing: bool Unsynchronized.ref
     1.8    val update: version_id -> version_id -> edit list -> state ->
     1.9      (command_id * exec_id option) list * state
    1.10    val state: unit -> state
    1.11 @@ -333,6 +334,9 @@
    1.12  
    1.13  (** document update **)
    1.14  
    1.15 +val timing = Unsynchronized.ref false;
    1.16 +fun timeit msg e = cond_timeit (! timing) msg e;
    1.17 +
    1.18  local
    1.19  
    1.20  fun stable_finished_theory node =
    1.21 @@ -447,13 +451,13 @@
    1.22    let
    1.23      val old_version = the_version state old_id;
    1.24      val _ = Time.now ();  (* FIXME odd workaround for polyml-5.4.0/x86_64 *)
    1.25 -    val new_version = fold edit_nodes edits old_version;
    1.26 +    val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version);
    1.27  
    1.28      val nodes = nodes_of new_version;
    1.29      val is_required = make_required nodes;
    1.30  
    1.31 -    val _ = terminate_execution state;
    1.32 -    val updated =
    1.33 +    val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state);
    1.34 +    val updated = timeit "Document.update" (fn () =>
    1.35        nodes |> Graph.schedule
    1.36          (fn deps => fn (name, node) =>
    1.37            (singleton o Future.forks)
    1.38 @@ -511,7 +515,7 @@
    1.39                    in ((no_execs, new_execs, updated_node), node') end
    1.40                  else (([], [], NONE), node)
    1.41                end))
    1.42 -      |> Future.joins |> map #1;
    1.43 +      |> Future.joins |> map #1);
    1.44  
    1.45      val command_execs =
    1.46        map (rpair NONE) (maps #1 updated) @