# HG changeset patch
# User wenzelm
# Date 1333540847 -7200
# Node ID 693276dcc51228dd16a5c0cdc19fe36b12dd93ed
# Parent  4708384e759dd0cb0e469edb8338ab31cf774959
tuned;

diff -r 4708384e759d -r 693276dcc512 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Apr 04 10:38:04 2012 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Apr 04 14:00:47 2012 +0200
@@ -243,7 +243,7 @@
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
-  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> name * span*)
+  commands: (string * Token.T list lazy) Inttab.table,  (*command_id -> named span*)
   execution: version_id * Future.group}  (*current execution process*)
 with
 
@@ -310,6 +310,12 @@
 
 local
 
+fun run int tr st =
+  (case Toplevel.transition int tr st of
+    SOME (st', NONE) => ([], SOME st')
+  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
+  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
+
 fun timing tr t =
   if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else ();
 
@@ -322,12 +328,6 @@
   (Lazy.lazy o Toplevel.setmp_thread_position tr)
     (fn () => Toplevel.print_state false st);
 
-fun run int tr st =
-  (case Toplevel.transition int tr st of
-    SOME (st', NONE) => ([], SOME st')
-  | SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE)
-  | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE));
-
 in
 
 fun run_command tr st =
@@ -363,7 +363,6 @@
 
 
 
-
 (** update **)
 
 (* perspective *)
@@ -380,6 +379,37 @@
 
 local
 
+fun make_required nodes =
+  let
+    val all_visible =
+      Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
+      |> Graph.all_preds nodes;
+    val required =
+      fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
+        all_visible Symtab.empty;
+  in Symtab.defined required end;
+
+fun init_theory deps node =
+  let
+    (* FIXME provide files via Scala layer, not master_dir *)
+    val (dir, header) = Exn.release (get_header node);
+    val master_dir =
+      (case Url.explode dir of
+        Url.File path => path
+      | _ => Path.current);
+    val parents =
+      #imports header |> map (fn import =>
+        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
+          SOME thy => thy
+        | NONE =>
+            get_theory (Position.file_only import)
+              (snd (Future.join (the (AList.lookup (op =) deps import))))));
+  in Thy_Load.begin_theory master_dir header parents end;
+
+fun check_theory nodes name =
+  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
+  is_some (Exn.get_res (get_header (get_node nodes name)));
+
 fun last_common state last_visible node0 node =
   let
     fun update_flags prev (visible, initial) =
@@ -428,37 +458,6 @@
       val command_exec' = (command_id', (exec_id', exec'));
     in SOME (command_exec' :: execs, command_exec', init') end;
 
-fun make_required nodes =
-  let
-    val all_visible =
-      Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes []
-      |> Graph.all_preds nodes;
-    val required =
-      fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ()))
-        all_visible Symtab.empty;
-  in Symtab.defined required end;
-
-fun check_theory nodes name =
-  is_some (Thy_Info.lookup_theory name) orelse  (* FIXME more robust!? *)
-  is_some (Exn.get_res (get_header (get_node nodes name)));
-
-fun init_theory deps node =
-  let
-    (* FIXME provide files via Scala layer, not master_dir *)
-    val (dir, header) = Exn.release (get_header node);
-    val master_dir =
-      (case Url.explode dir of
-        Url.File path => path
-      | _ => Path.current);
-    val parents =
-      #imports header |> map (fn import =>
-        (case Thy_Info.lookup_theory import of  (* FIXME more robust!? *)
-          SOME thy => thy
-        | NONE =>
-            get_theory (Position.file_only import)
-              (snd (Future.join (the (AList.lookup (op =) deps import))))));
-  in Thy_Load.begin_theory master_dir header parents end;
-
 in
 
 fun update (old_id: version_id) (new_id: version_id) edits state =