more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
authorwenzelm
Fri Nov 22 20:28:49 2013 +0100 (2013-11-22)
changeset 5455831844ca390ad
parent 54557 d71c2737ee21
child 54559 39d91cac6e91
more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Nov 22 13:42:00 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Nov 22 20:28:49 2013 +0100
     1.3 @@ -81,6 +81,11 @@
     1.4  
     1.5  (* basic components *)
     1.6  
     1.7 +fun master_directory (Node {header = (master, _, _), ...}) =
     1.8 +  (case try Url.explode master of
     1.9 +    SOME (Url.File path) => path
    1.10 +  | _ => Path.current);
    1.11 +
    1.12  fun set_header header =
    1.13    map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result));
    1.14  
    1.15 @@ -94,11 +99,6 @@
    1.16      val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
    1.17    in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
    1.18  
    1.19 -fun master_directory node =
    1.20 -  (case try Url.explode (#1 (get_header node)) of
    1.21 -    SOME (Url.File path) => path
    1.22 -  | _ => Path.current);
    1.23 -
    1.24  fun get_perspective (Node {perspective, ...}) = perspective;
    1.25  fun set_perspective args =
    1.26    map_node (fn (header, _, entries, result) => (header, make_perspective args, entries, result));