tuned according to Scala version;
authorwenzelm
Wed Apr 12 23:35:42 2017 +0200 (2017-04-12 ago)
changeset 654745624e9694915
parent 65473 b47373f52451
child 65475 4519c8cc4bec
tuned according to Scala version;
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Wed Apr 12 23:08:24 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Wed Apr 12 23:35:42 2017 +0200
     1.3 @@ -108,25 +108,26 @@
     1.4      SOME qualifier => qualifier
     1.5    | NONE => Long_Name.qualifier theory);
     1.6  
     1.7 -fun theory_name qualifier theory0 =
     1.8 +fun loaded_theory_name qualifier theory0 =
     1.9    (case loaded_theory theory0 of
    1.10      SOME theory => (true, theory)
    1.11    | NONE =>
    1.12 -      (false,
    1.13 +      let val theory =
    1.14          if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    1.15            orelse true (* FIXME *) then theory0
    1.16 -        else Long_Name.qualify qualifier theory0));
    1.17 +        else Long_Name.qualify qualifier theory0
    1.18 +      in (false, theory) end);
    1.19  
    1.20  fun import_name qualifier dir s =
    1.21 -  let
    1.22 -    val (loaded, theory) = theory_name qualifier (Thy_Header.import_name s);
    1.23 -    val node_name =
    1.24 -      if loaded then Path.basic theory
    1.25 -      else
    1.26 +  (case loaded_theory_name qualifier (Thy_Header.import_name s) of
    1.27 +    (true, theory) =>
    1.28 +      {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
    1.29 +  | (false, theory) =>
    1.30 +      let val node_name =
    1.31          (case known_theory theory of
    1.32            SOME node_name => node_name
    1.33 -        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))));
    1.34 -  in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end;
    1.35 +        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))))
    1.36 +      in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end);
    1.37  
    1.38  fun check_file dir file = File.check_file (File.full_path dir file);
    1.39