# HG changeset patch
# User wenzelm
# Date 1429112085 -7200
# Node ID 9fb7b44e3e7e4df93b61e245cbdcbe1f0939e16f
# Parent  019347f8dc88b532d5ed64d2b3d48f15576d3acd
tuned signature;

diff -r 019347f8dc88 -r 9fb7b44e3e7e src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Wed Apr 15 15:57:58 2015 +0200
+++ b/src/Pure/PIDE/session.ML	Wed Apr 15 17:34:45 2015 +0200
@@ -6,7 +6,7 @@
 
 signature SESSION =
 sig
-  val name: unit -> string
+  val get_name: unit -> string
   val welcome: unit -> string
   val get_keywords: unit -> Keyword.keywords
   val init: bool -> bool -> Path.T -> string -> string -> (string * string) list ->
@@ -26,12 +26,14 @@
 val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
 val session_finished = Unsynchronized.ref false;
 
-fun name () = "Isabelle/" ^ #name (! session);
+fun get_name () = #name (! session);
+
+fun description () = "Isabelle/" ^ get_name ();
 
 fun welcome () =
   if Distribution.is_identified then
-    "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
-  else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
+    "Welcome to " ^ description () ^ " (" ^ Distribution.version ^ ")"
+  else "Unofficial version of " ^ description () ^ " (" ^ Distribution.version ^ ")";
 
 
 (* base syntax *)
@@ -44,7 +46,7 @@
 
 fun init build info info_path doc doc_output doc_variants doc_files graph_file
     parent (chapter, name) verbose =
-  if #name (! session) <> parent orelse not (! session_finished) then
+  if get_name () <> parent orelse not (! session_finished) then
     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
   else
     let