src/Pure/PIDE/document.ML
changeset 41537 3837045cc8a1
parent 40534 9e196062bf88
child 41629 5490dc4d999d
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Jan 13 17:34:45 2011 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Jan 13 17:39:35 2011 +0100
     1.3 @@ -214,12 +214,16 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun run_command thy_name tr st =
     1.8 +fun run_command thy_name raw_tr st =
     1.9    (case
    1.10 -      (case Toplevel.init_of tr of
    1.11 -        SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
    1.12 -      | NONE => Exn.Result ()) of
    1.13 -    Exn.Result () =>
    1.14 +      (case Toplevel.init_of raw_tr of
    1.15 +        SOME name => Exn.capture (fn () =>
    1.16 +          let
    1.17 +            val path = Path.explode thy_name;
    1.18 +            val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
    1.19 +          in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
    1.20 +      | NONE => Exn.Result raw_tr) of
    1.21 +    Exn.Result tr =>
    1.22        let
    1.23          val is_init = is_some (Toplevel.init_of tr);
    1.24          val is_proof = Keyword.is_proof (Toplevel.name_of tr);
    1.25 @@ -241,8 +245,8 @@
    1.26    | Exn.Exn exn =>
    1.27        if Exn.is_interrupt exn then reraise exn
    1.28        else
    1.29 -       (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
    1.30 -        Toplevel.status tr Markup.failed;
    1.31 +       (Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn);
    1.32 +        Toplevel.status raw_tr Markup.failed;
    1.33          (false, Toplevel.toplevel)));
    1.34  
    1.35  end;