src/Pure/PIDE/resources.ML
changeset 65457 2bf0d2fcd506
parent 65454 2b22b7d8649f
child 65471 05e5bffcf1d8
     1.1 --- a/src/Pure/PIDE/resources.ML	Mon Apr 10 13:30:55 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Mon Apr 10 16:43:12 2017 +0200
     1.3 @@ -8,12 +8,12 @@
     1.4  sig
     1.5    val set_session_base:
     1.6      {default_qualifier: string,
     1.7 -     global_theories: string list,
     1.8 +     global_theories: (string * string) list,
     1.9       loaded_theories: (string * string) list,
    1.10       known_theories: (string * string) list} -> unit
    1.11    val reset_session_base: unit -> unit
    1.12    val default_qualifier: unit -> string
    1.13 -  val global_theory: string -> bool
    1.14 +  val global_theory: string -> string option
    1.15    val loaded_theory: string -> Path.T option
    1.16    val known_theory: string -> Path.T option
    1.17    val master_directory: theory -> Path.T
    1.18 @@ -42,7 +42,7 @@
    1.19  
    1.20  val init_session_base =
    1.21    {default_qualifier = "Draft",
    1.22 -   global_theories = Symtab.make_set [],
    1.23 +   global_theories = Symtab.empty: string Symtab.table,
    1.24     loaded_theories = Symtab.empty: Path.T Symtab.table,
    1.25     known_theories = Symtab.empty: Path.T Symtab.table};
    1.26  
    1.27 @@ -55,7 +55,7 @@
    1.28        {default_qualifier =
    1.29          if default_qualifier <> "" then default_qualifier
    1.30          else #default_qualifier init_session_base,
    1.31 -       global_theories = Symtab.make_set global_theories,
    1.32 +       global_theories = Symtab.make global_theories,
    1.33         loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
    1.34         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    1.35  
    1.36 @@ -65,7 +65,7 @@
    1.37  fun get_session_base f = f (Synchronized.value global_session_base);
    1.38  
    1.39  fun default_qualifier () = get_session_base #default_qualifier;
    1.40 -fun global_theory a = Symtab.defined (get_session_base #global_theories) a;
    1.41 +fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
    1.42  fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
    1.43  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
    1.44  
    1.45 @@ -104,13 +104,15 @@
    1.46  val thy_path = Path.ext "thy";
    1.47  
    1.48  fun theory_qualifier theory =
    1.49 -  Long_Name.qualifier theory;
    1.50 +  (case global_theory theory of
    1.51 +    SOME qualifier => qualifier
    1.52 +  | NONE => Long_Name.qualifier theory);
    1.53  
    1.54  fun import_name qualifier dir s =
    1.55    let
    1.56      val theory0 = Thy_Header.import_name s;
    1.57      val theory =
    1.58 -      if Long_Name.is_qualified theory0 orelse global_theory theory0
    1.59 +      if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
    1.60          orelse true (* FIXME *) then theory0
    1.61        else Long_Name.qualify qualifier theory0;
    1.62      val node_name =