# 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 =