src/Pure/PIDE/document.ML
changeset 44160 8848867501fb
parent 44157 a21d3e1e64fd
child 44180 a6dc270d3edb
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 12 12:03:17 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 12 15:28:30 2011 +0200
     1.3 @@ -249,14 +249,13 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun run_command thy_name raw_tr st =
     1.8 +fun run_command node_name raw_tr st =
     1.9    (case
    1.10        (case Toplevel.init_of raw_tr of
    1.11 -        SOME name => Exn.capture (fn () =>
    1.12 -          let
    1.13 -            val path = Path.explode thy_name;
    1.14 -            val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
    1.15 -          in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
    1.16 +        SOME name =>
    1.17 +          Exn.capture (fn () =>
    1.18 +            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
    1.19 +            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
    1.20        | NONE => Exn.Res raw_tr) of
    1.21      Exn.Res tr =>
    1.22        let