clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
authorwenzelm
Thu Apr 13 12:39:36 2017 +0200 (2017-04-13 ago)
changeset 654787c40477e0a87
parent 65477 64e61b0f6972
child 65479 7ca8810b1d48
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
src/Pure/ML/ml_process.scala
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/resources.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/ML/ml_process.scala	Thu Apr 13 12:27:57 2017 +0200
     1.2 +++ b/src/Pure/ML/ml_process.scala	Thu Apr 13 12:39:36 2017 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4              ML_Syntax.print_list(
     1.5                ML_Syntax.print_pair(
     1.6                  ML_Syntax.print_string, ML_Syntax.print_string))(table)
     1.7 -          List("Resources.set_session_base {default_qualifier = \"\"" +
     1.8 +          List("Resources.init_session_base {default_qualifier = \"\"" +
     1.9              ", global_theories = " + print_table(base.global_theories.toList) +
    1.10              ", loaded_theories = " + print_table(base.loaded_theories.toList) +
    1.11              ", known_theories = " + print_table(base.dest_known_theories) + "}")
     2.1 --- a/src/Pure/PIDE/protocol.ML	Thu Apr 13 12:27:57 2017 +0200
     2.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Apr 13 12:39:36 2017 +0200
     2.3 @@ -23,7 +23,7 @@
     2.4        let
     2.5          val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
     2.6        in
     2.7 -        Resources.set_session_base
     2.8 +        Resources.init_session_base
     2.9            {default_qualifier = default_qualifier,
    2.10             global_theories = decode_table global_theories_yxml,
    2.11             loaded_theories = decode_table loaded_theories_yxml,
     3.1 --- a/src/Pure/PIDE/resources.ML	Thu Apr 13 12:27:57 2017 +0200
     3.2 +++ b/src/Pure/PIDE/resources.ML	Thu Apr 13 12:39:36 2017 +0200
     3.3 @@ -6,12 +6,12 @@
     3.4  
     3.5  signature RESOURCES =
     3.6  sig
     3.7 -  val set_session_base:
     3.8 +  val init_session_base:
     3.9      {default_qualifier: string,
    3.10       global_theories: (string * string) list,
    3.11       loaded_theories: (string * string) list,
    3.12       known_theories: (string * string) list} -> unit
    3.13 -  val reset_session_base: unit -> unit
    3.14 +  val finish_session_base: unit -> unit
    3.15    val default_qualifier: unit -> string
    3.16    val global_theory: string -> string option
    3.17    val loaded_theory: string -> string option
    3.18 @@ -40,27 +40,32 @@
    3.19  
    3.20  (* session base *)
    3.21  
    3.22 -val init_session_base =
    3.23 +val empty_session_base =
    3.24    {default_qualifier = "Draft",
    3.25     global_theories = Symtab.empty: string Symtab.table,
    3.26     loaded_theories = Symtab.empty: string Symtab.table,
    3.27     known_theories = Symtab.empty: Path.T Symtab.table};
    3.28  
    3.29  val global_session_base =
    3.30 -  Synchronized.var "Sessions.base" init_session_base;
    3.31 +  Synchronized.var "Sessions.base" empty_session_base;
    3.32  
    3.33 -fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
    3.34 +fun init_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
    3.35    Synchronized.change global_session_base
    3.36      (fn _ =>
    3.37        {default_qualifier =
    3.38          if default_qualifier <> "" then default_qualifier
    3.39 -        else #default_qualifier init_session_base,
    3.40 +        else #default_qualifier empty_session_base,
    3.41         global_theories = Symtab.make global_theories,
    3.42         loaded_theories = Symtab.make loaded_theories,
    3.43         known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
    3.44  
    3.45 -fun reset_session_base () =
    3.46 -  Synchronized.change global_session_base (K init_session_base);
    3.47 +fun finish_session_base () =
    3.48 +  Synchronized.change global_session_base
    3.49 +    (fn {global_theories, loaded_theories, ...} =>
    3.50 +      {default_qualifier = #default_qualifier empty_session_base,
    3.51 +       global_theories = global_theories,
    3.52 +       loaded_theories = loaded_theories,
    3.53 +       known_theories = #known_theories empty_session_base});
    3.54  
    3.55  fun get_session_base f = f (Synchronized.value global_session_base);
    3.56  
     4.1 --- a/src/Pure/Tools/build.ML	Thu Apr 13 12:27:57 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.ML	Thu Apr 13 12:39:36 2017 +0200
     4.3 @@ -180,7 +180,7 @@
     4.4      val symbols = HTML.make_symbols symbol_codes;
     4.5  
     4.6      val _ =
     4.7 -      Resources.set_session_base
     4.8 +      Resources.init_session_base
     4.9          {default_qualifier = name,
    4.10           global_theories = global_theories,
    4.11           loaded_theories = loaded_theories,
    4.12 @@ -210,7 +210,7 @@
    4.13            |> Exn.capture);
    4.14      val res2 = Exn.capture Session.finish ();
    4.15  
    4.16 -    val _ = Resources.reset_session_base ();
    4.17 +    val _ = Resources.finish_session_base ();
    4.18      val _ = Par_Exn.release_all [res1, res2];
    4.19    in () end;
    4.20