# HG changeset patch
# User paulson
# Date 938529862 -7200
# Node ID 8e177a4c86a51971b2ec58cd981ff5707aa1961d
# Parent  6b0709a2f6c7a4799962287fad72b5dbc80be6fe
tidied, using "warning" function and fixing the Close_locale bug

diff -r 6b0709a2f6c7 -r 8e177a4c86a5 src/Pure/locale.ML
--- a/src/Pure/locale.ML	Tue Sep 28 16:37:04 1999 +0200
+++ b/src/Pure/locale.ML	Tue Sep 28 16:44:22 1999 +0200
@@ -191,8 +191,8 @@
        | Some(loc') => 
            if loc' mem (map fst cur_sc) 
            then opn loc thy
-           else (Pretty.writeln(Pretty.str 
-                   ("Opening locale " ^ quote loc' ^ ", required by " ^ quote xname));
+           else (warning ("Opening locale " ^ quote loc' ^ ", required by " ^ 
+			  quote xname);
                  opn loc (open_locale (Sign.base_name loc') thy))
   end;
 
@@ -200,12 +200,11 @@
   | pop_locale (_ :: locs) = locs;
 
 fun close_locale name thy = 
-   let val cur_sc = get_scope thy;
-       val lname = if null(cur_sc) then "" else (fst (hd cur_sc));
-       val bname = Sign.base_name lname
-   in if (name = bname) then (change_scope pop_locale thy; thy)
-      else (Pretty.writeln(Pretty.str ("locale " ^ name ^ " is not top of scope"));
-            Pretty.writeln(Pretty.str ("Command has no effect, top is " ^ lname)); thy)
+   let val lname = (case get_scope thy of (ln,_)::_ => ln
+                                        | _ => error "No locales are open!")
+       val ok = (name = Sign.base_name lname) handle _ => false
+   in if ok then (change_scope pop_locale thy; thy)
+      else error ("locale " ^ name ^ " is not top of scope; top is " ^ lname)
    end;
 
 fun print_scope thy =