full theory path enables loading parents via master directory and keeps files strictly separate;
authorwenzelm
Thu Jan 13 17:39:35 2011 +0100 (2011-01-13)
changeset 415373837045cc8a1
parent 41536 47fef6afe756
child 41538 d060ccad02bd
full theory path enables loading parents via master directory and keeps files strictly separate;
src/Pure/PIDE/document.ML
src/Tools/jEdit/src/jedit/plugin.scala
     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;
     2.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Jan 13 17:34:45 2011 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Jan 13 17:39:35 2011 +0100
     2.3 @@ -266,8 +266,8 @@
     2.4            case Some(model) => model.refresh; Some(model)
     2.5            case None =>
     2.6              Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
     2.7 -              case Some((_, thy_name)) =>
     2.8 -                Some(Document_Model.init(Isabelle.session, buffer, thy_name))
     2.9 +              case Some((dir, thy_name)) =>
    2.10 +                Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
    2.11                case None => None
    2.12              }
    2.13          }