# HG changeset patch
# User wenzelm
# Date 1385148529 -3600
# Node ID 31844ca390ada9e32b2372f2fa85099f3173d9df
# Parent  d71c2737ee2149e5ee251aa521a835cb83219ebd
more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);

diff -r d71c2737ee21 -r 31844ca390ad src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 22 13:42:00 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 22 20:28:49 2013 +0100
@@ -81,6 +81,11 @@
 
 (* basic components *)
 
+fun master_directory (Node {header = (master, _, _), ...}) =
+  (case try Url.explode master of
+    SOME (Url.File path) => path
+  | _ => Path.current);
+
 fun set_header header =
   map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
 
@@ -94,11 +99,6 @@
     val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
   in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
 
-fun master_directory node =
-  (case try Url.explode (#1 (get_header node)) of
-    SOME (Url.File path) => path
-  | _ => Path.current);
-
 fun get_perspective (Node {perspective, ...}) = perspective;
 fun set_perspective args =
   map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));