src/Pure/PIDE/resources.ML
changeset 65532 febfd9f78bd4
parent 65505 741fad555d82
child 66711 80fa1401cf76
     1.1 --- a/src/Pure/PIDE/resources.ML	Fri Apr 21 13:51:43 2017 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Fri Apr 21 14:09:03 2017 +0200
     1.3 @@ -6,13 +6,12 @@
     1.4  
     1.5  signature RESOURCES =
     1.6  sig
     1.7 +  val default_qualifier: string
     1.8    val init_session_base:
     1.9 -    {default_qualifier: string,
    1.10 -     global_theories: (string * string) list,
    1.11 +    {global_theories: (string * string) list,
    1.12       loaded_theories: (string * string) list,
    1.13       known_theories: (string * string) list} -> unit
    1.14    val finish_session_base: unit -> unit
    1.15 -  val default_qualifier: unit -> string
    1.16    val global_theory: string -> string option
    1.17    val loaded_theory: string -> string option
    1.18    val known_theory: string -> Path.T option
    1.19 @@ -37,36 +36,32 @@
    1.20  
    1.21  (* session base *)
    1.22  
    1.23 +val default_qualifier = "Draft";
    1.24 +
    1.25  val empty_session_base =
    1.26 -  {default_qualifier = "Draft",
    1.27 -   global_theories = Symtab.empty: string Symtab.table,
    1.28 +  {global_theories = Symtab.empty: string Symtab.table,
    1.29     loaded_theories = Symtab.empty: string Symtab.table,
    1.30     known_theories = Symtab.empty: Path.T Symtab.table};
    1.31  
    1.32  val global_session_base =
    1.33    Synchronized.var "Sessions.base" empty_session_base;
    1.34  
    1.35 -fun init_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
    1.36 +fun init_session_base {global_theories, loaded_theories, known_theories} =
    1.37    Synchronized.change global_session_base
    1.38      (fn _ =>
    1.39 -      {default_qualifier =
    1.40 -        if default_qualifier <> "" then default_qualifier
    1.41 -        else #default_qualifier empty_session_base,
    1.42 -       global_theories = Symtab.make global_theories,
    1.43 +      {global_theories = Symtab.make global_theories,
    1.44         loaded_theories = Symtab.make loaded_theories,
    1.45         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    1.46  
    1.47  fun finish_session_base () =
    1.48    Synchronized.change global_session_base
    1.49      (fn {global_theories, loaded_theories, ...} =>
    1.50 -      {default_qualifier = #default_qualifier empty_session_base,
    1.51 -       global_theories = global_theories,
    1.52 +      {global_theories = global_theories,
    1.53         loaded_theories = loaded_theories,
    1.54         known_theories = #known_theories empty_session_base});
    1.55  
    1.56  fun get_session_base f = f (Synchronized.value global_session_base);
    1.57  
    1.58 -fun default_qualifier () = get_session_base #default_qualifier;
    1.59  fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
    1.60  fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
    1.61  fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;