src/Pure/PIDE/resources.ML
changeset 65471 05e5bffcf1d8
parent 65457 2bf0d2fcd506
child 65474 5624e9694915
     1.1 --- a/src/Pure/PIDE/resources.ML	Wed Apr 12 21:13:43 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Wed Apr 12 22:32:55 2017 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val reset_session_base: unit -> unit
     1.5    val default_qualifier: unit -> string
     1.6    val global_theory: string -> string option
     1.7 -  val loaded_theory: string -> Path.T option
     1.8 +  val loaded_theory: string -> string option
     1.9    val known_theory: string -> Path.T option
    1.10    val master_directory: theory -> Path.T
    1.11    val imports_of: theory -> (string * Position.T) list
    1.12 @@ -43,7 +43,7 @@
    1.13  val init_session_base =
    1.14    {default_qualifier = "Draft",
    1.15     global_theories = Symtab.empty: string Symtab.table,
    1.16 -   loaded_theories = Symtab.empty: Path.T Symtab.table,
    1.17 +   loaded_theories = Symtab.empty: string Symtab.table,
    1.18     known_theories = Symtab.empty: Path.T Symtab.table};
    1.19  
    1.20  val global_session_base =
    1.21 @@ -56,7 +56,7 @@
    1.22          if default_qualifier <> "" then default_qualifier
    1.23          else #default_qualifier init_session_base,
    1.24         global_theories = Symtab.make global_theories,
    1.25 -       loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
    1.26 +       loaded_theories = Symtab.make loaded_theories,
    1.27         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    1.28  
    1.29  fun reset_session_base () =
    1.30 @@ -108,20 +108,24 @@
    1.31      SOME qualifier => qualifier
    1.32    | NONE => Long_Name.qualifier theory);
    1.33  
    1.34 +fun theory_name qualifier theory0 =
    1.35 +  (case loaded_theory theory0 of
    1.36 +    SOME theory => (true, theory)
    1.37 +  | NONE =>
    1.38 +      (false,
    1.39 +        if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    1.40 +          orelse true (* FIXME *) then theory0
    1.41 +        else Long_Name.qualify qualifier theory0));
    1.42 +
    1.43  fun import_name qualifier dir s =
    1.44    let
    1.45 -    val theory0 = Thy_Header.import_name s;
    1.46 -    val theory =
    1.47 -      if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    1.48 -        orelse true (* FIXME *) then theory0
    1.49 -      else Long_Name.qualify qualifier theory0;
    1.50 +    val (loaded, theory) = theory_name qualifier (Thy_Header.import_name s);
    1.51      val node_name =
    1.52 -      the (get_first (fn e => e ())
    1.53 -        [fn () => loaded_theory theory,
    1.54 -         fn () => loaded_theory theory0,
    1.55 -         fn () => known_theory theory,
    1.56 -         fn () => known_theory theory0,
    1.57 -         fn () => SOME (File.full_path dir (thy_path (Path.expand (Path.explode s))))])
    1.58 +      if loaded then Path.basic theory
    1.59 +      else
    1.60 +        (case known_theory theory of
    1.61 +          SOME node_name => node_name
    1.62 +        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))));
    1.63    in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end;
    1.64  
    1.65  fun check_file dir file = File.check_file (File.full_path dir file);