# HG changeset patch
# User wenzelm
# Date 964346887 -7200
# Node ID 1463576f39684885e6bdd0d667aa848eb0a553cb
# Parent  ba209591a8d4b215afe1d0979dedf926514d254c
disallow duplicates in session identifiers;

diff -r ba209591a8d4 -r 1463576f3968 src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Sun Jul 23 12:06:46 2000 +0200
+++ b/src/Pure/Isar/session.ML	Sun Jul 23 12:08:07 2000 +0200
@@ -24,22 +24,29 @@
 val session = ref ([pure]: string list);
 val session_path = ref ([]: string list);
 val session_finished = ref false;
-val rpath = ref (None : Url.T option);
+val rpath = ref (None: Url.T option);
+
+
+(* access path *)
 
 fun path () = ! session_path;
 
-fun add_path reset s =
-  (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
-
-
-(* diagnostics *)
-
 fun str_of [] = "Pure"
   | str_of elems = space_implode "/" elems;
 
 fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
 
 
+(* add_path *)
+
+fun add_path reset s =
+  let val sess = ! session @ [s] in
+    (case Library.duplicates sess of
+      [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
+    | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
+  end;
+
+
 (* init *)
 
 fun init reset parent name =