src/Pure/PIDE/resources.ML
changeset 66712 4c98c929a12a
parent 66711 80fa1401cf76
child 66771 925d10a7a610
     1.1 --- a/src/Pure/PIDE/resources.ML	Thu Sep 28 11:53:55 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Thu Sep 28 15:11:32 2017 +0200
     1.3 @@ -9,11 +9,11 @@
     1.4    val default_qualifier: string
     1.5    val init_session_base:
     1.6      {global_theories: (string * string) list,
     1.7 -     loaded_theories: (string * string) list,
     1.8 +     loaded_theories: string list,
     1.9       known_theories: (string * string) list} -> unit
    1.10    val finish_session_base: unit -> unit
    1.11    val global_theory: string -> string option
    1.12 -  val loaded_theory: string -> string option
    1.13 +  val loaded_theory: string -> bool
    1.14    val known_theory: string -> Path.T option
    1.15    val master_directory: theory -> Path.T
    1.16    val imports_of: theory -> (string * Position.T) list
    1.17 @@ -39,7 +39,7 @@
    1.18  
    1.19  val empty_session_base =
    1.20    {global_theories = Symtab.empty: string Symtab.table,
    1.21 -   loaded_theories = Symtab.empty: string Symtab.table,
    1.22 +   loaded_theories = Symtab.empty: unit Symtab.table,
    1.23     known_theories = Symtab.empty: Path.T Symtab.table};
    1.24  
    1.25  val global_session_base =
    1.26 @@ -49,7 +49,7 @@
    1.27    Synchronized.change global_session_base
    1.28      (fn _ =>
    1.29        {global_theories = Symtab.make global_theories,
    1.30 -       loaded_theories = Symtab.make loaded_theories,
    1.31 +       loaded_theories = Symtab.make_set loaded_theories,
    1.32         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    1.33  
    1.34  fun finish_session_base () =
    1.35 @@ -62,7 +62,7 @@
    1.36  fun get_session_base f = f (Synchronized.value global_session_base);
    1.37  
    1.38  fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
    1.39 -fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
    1.40 +fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
    1.41  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    1.42  
    1.43  
    1.44 @@ -107,15 +107,14 @@
    1.45      SOME qualifier => qualifier
    1.46    | NONE => Long_Name.qualifier theory);
    1.47  
    1.48 -fun theory_name qualifier theory0 =
    1.49 -  (case loaded_theory theory0 of
    1.50 -    SOME theory => (true, theory)
    1.51 -  | NONE =>
    1.52 -      let val theory =
    1.53 -        if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    1.54 -        then theory0
    1.55 -        else Long_Name.qualify qualifier theory0
    1.56 -      in (false, theory) end);
    1.57 +fun theory_name qualifier theory =
    1.58 +  if loaded_theory theory then (true, theory)
    1.59 +  else
    1.60 +    let val theory' =
    1.61 +      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
    1.62 +      then theory
    1.63 +      else Long_Name.qualify qualifier theory
    1.64 +    in (false, theory') end;
    1.65  
    1.66  fun import_name qualifier dir s =
    1.67    (case theory_name qualifier (Thy_Header.import_name s) of