# HG changeset patch
# User wenzelm
# Date 1314127164 -7200
# Node ID d4c69d0bbd27e8c264b006a81a2dabbb9bfe565f
# Parent  3b9b684bfa6fe5e2dfc9be664419216a5f91499d
tuned;

diff -r 3b9b684bfa6f -r d4c69d0bbd27 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Aug 23 21:14:59 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Tue Aug 23 21:19:24 2011 +0200
@@ -329,6 +329,24 @@
     NONE => true
   | SOME exec' => exec' <> exec);
 
+fun init_theory deps (name, node) =
+  let
+    val (thy_name, imports, uses) = Exn.release (get_header node);
+    (* FIXME provide files via Scala layer *)
+    val (dir, files) =
+      if ML_System.platform_is_cygwin then (Path.current, [])
+      else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
+
+    val parents =
+      imports |> map (fn import =>
+        (case Thy_Info.lookup_theory import of
+          SOME thy => thy
+        | NONE =>
+            get_theory (Position.file_only import)
+              (#2 (Future.join (the (AList.lookup (op =) deps import))))));
+  in Thy_Load.begin_theory dir thy_name imports files parents end;
+
+
 fun new_exec (command_id, command) (assigns, execs, exec) =
   let
     val exec_id' = new_id ();
@@ -352,22 +370,7 @@
             NONE => Future.value (([], [], []), node)
           | SOME ((prev, id), _) =>
               let
-                fun init () =
-                  let
-                    val (thy_name, imports, uses) = Exn.release (get_header node);
-                    (* FIXME provide files via Scala layer *)
-                    val (dir, files) =
-                      if ML_System.platform_is_cygwin then (Path.current, [])
-                      else (Path.dir (Path.explode name), map (apfst Path.explode) uses);
-
-                    val parents =
-                      imports |> map (fn import =>
-                        (case Thy_Info.lookup_theory import of
-                          SOME thy => thy
-                        | NONE =>
-                            get_theory (Position.file_only import)
-                              (#2 (Future.join (the (AList.lookup (op =) deps import))))));
-                  in Thy_Load.begin_theory dir thy_name imports files parents end;
+                fun init () = init_theory deps (name, node);
                 fun get_command id =
                   (id, the_command state id |> Future.map (Toplevel.modify_init init));
               in