src/Pure/System/session.ML

 (*  Title:      Pure/System/session.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Session management -- maintain state of logic images.
+Session management -- internal state of logic images.
 *)
 
 signature SESSION =
 sig
-  val id: unit -> string list
   val name: unit -> string
-  val path: unit -> string list
   val welcome: unit -> string
+  val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
+    string -> string * string -> bool * string -> bool -> unit
   val finish: unit -> unit
-  val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
-    string -> string -> bool * string -> bool -> unit
   val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
     string -> int -> bool -> bool -> int -> int -> int -> int -> unit
 end;

 structure Session: SESSION =
 struct
 
 (* session state *)
 
-val session = Unsynchronized.ref ([Context.PureN]: string list);
+val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
 val session_finished = Unsynchronized.ref false;
 
-fun id () = ! session;
-fun name () = "Isabelle/" ^ List.last (! session);
-
-
-(* access path *)
-
-val session_path = Unsynchronized.ref ([]: string list);
-
-fun path () = ! session_path;
-
-
-(* welcome *)
+fun name () = "Isabelle/" ^ #name (! session);
 
 fun welcome () =
   if Distribution.is_official then
     "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
   else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
 
 
-(* add_path *)
+(* init *)
 
-fun add_path reset s =
-  let val sess = ! session @ [s] in
-    (case duplicates (op =) sess of
-      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
-    | dups => error ("Duplicate session identifiers " ^ commas_quote dups))
-  end;
-
-
-(* init_name *)
-
-fun init_name reset parent name =
-  if not (member (op =) (! session) parent) orelse not (! session_finished) then
+fun init build info info_path doc doc_graph doc_output doc_variants
+    parent (chapter, name) doc_dump verbose =
+  if #name (! session) <> parent orelse not (! session_finished) then
     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
-  else (add_path reset name; session_finished := false);
+  else
+    let
+      val _ = session := {chapter = chapter, name = name};
+      val _ = session_finished := false;
+    in
+      Present.init build info info_path (if doc = "false" then "" else doc)
+        doc_graph doc_output doc_variants (chapter, name)
+        doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
+    end;
 
 
 (* finish *)
 
 fun finish () =

   Options.reset_default ();
   Future.shutdown ();
   session_finished := true);
 
 
-(* use_dir *)
+(* timing within ML *)
 
 fun with_timing name verbose f x =
   let
     val start = Timing.start ();
     val y = f x;

         Output.physical_stderr ("Timing " ^ name ^ " (" ^
           threads ^ " threads, " ^ Timing.message timing ^ ", factor " ^ factor ^ ")\n")
       else ();
   in y end;
 
-fun init build reset info info_path doc doc_graph doc_output doc_variants
-    parent name doc_dump verbose =
- (init_name reset parent name;
-  Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_output
-    doc_variants (path ()) name doc_dump verbose
-    (map Thy_Info.get_theory (Thy_Info.get_names ())));
 
-local
+(* use_dir *)
 
 fun read_variants strs =
   rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
   |> filter_out (fn (_, s) => s = "-");
-
-in
 
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name doc_dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
     let
       val _ =
         Output.physical_stderr
           "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
       val _ =
+        if not reset then ()
+        else Output.physical_stderr "### Ignoring reset (historic usedir option -r)\n";
+      val _ =
         if rpath = "" then ()
-        else
-          Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
+        else Output.physical_stderr "### Ignoring remote path (historic usedir option -P)\n";
 
       val _ =
-        init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
-          doc_dump verbose;
+        init build info (Path.explode info_path) doc doc_graph "" (read_variants doc_variants)
+          parent ("Unsorted", name) doc_dump verbose;
       val res1 = (use |> with_timing item timing |> Exn.capture) root;
       val res2 = Exn.capture finish ();
     in ignore (Par_Exn.release_all [res1, res2]) end)
     |> Unsynchronized.setmp Proofterm.proofs level
     |> Unsynchronized.setmp print_mode (modes @ print_mode_value ())

       (if Multithreading.available then max_threads
        else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
 
 end;
-
-end;