--- a/src/Pure/Syntax/parser.ML Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/Syntax/parser.ML Fri Mar 15 12:01:19 1996 +0100
@@ -752,7 +752,7 @@
val dummy =
if not (!warned) andalso
length (new_states @ States) > (!branching_level) then
- (writeln "Warning: Currently parsed expression could be \
+ (warning "Currently parsed expression could be \
\extremely ambiguous.";
warned := true)
else ();
--- a/src/Pure/Syntax/syntax.ML Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/Syntax/syntax.ML Fri Mar 15 12:01:19 1996 +0100
@@ -308,7 +308,7 @@
fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
in
if length pts > ! ambiguity_level then
- (writeln ("Warning: Ambiguous input " ^ quote str);
+ (warning ("Ambiguous input " ^ quote str);
writeln "produces the following parse trees:";
seq show_pt pts)
else ();
--- a/src/Pure/Thy/thm_database.ML Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/Thy/thm_database.ML Fri Mar 15 12:01:19 1996 +0100
@@ -86,7 +86,7 @@
end;
val const_idx' = update_db false consts const_idx;
- in if consts = [] then writeln ("Warning: Theorem " ^ name ^
+ in if consts = [] then warning ("Theorem " ^ name ^
" cannot be stored in ThmDB\n\t because it \
\contains no or only ignored constants.")
else if is_some const_idx' then
--- a/src/Pure/Thy/thy_read.ML Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/Thy/thy_read.ML Fri Mar 15 12:01:19 1996 +0100
@@ -299,7 +299,7 @@
else (find_file abs_path (name ^ ".thy"),
find_file abs_path (name ^ ".ML"))
in if thy_file = "" andalso ml_file = "" then
- (writeln ("Warning: File \"" ^ (tack_on path name)
+ (warning ("File \"" ^ (tack_on path name)
^ ".thy\"\ncontaining theory \"" ^ name
^ "\" no longer exists.");
new_filename ()
@@ -543,7 +543,7 @@
in mk_entry relatives end;
in if is_some (!cur_htmlfile) then
(close_out (the (!cur_htmlfile));
- writeln "Warning: Last theory's HTML file has not been closed.")
+ warning "Last theory's HTML file has not been closed.")
else ();
cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html")));
cur_has_title := false;
@@ -668,7 +668,7 @@
val fname = tack_on path ("." ^ t ^ "_sub.html");
val out = if file_exists fname then
open_append fname handle Io s =>
- (writeln ("Warning: Unable to write to file ." ^
+ (warning ("Unable to write to file ." ^
fname); raise Io s)
else raise MK_HTML;
in output (out,
@@ -1039,7 +1039,7 @@
val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
handle Symtab.DUPLICATE s =>
(if eq_thm (the (Symtab.lookup (thms, name)), thm) then
- (writeln ("Warning: Theory database already contains copy of\
+ (warning ("Theory database already contains copy of\
\ theorem " ^ quote name);
(thms, true))
else error ("Duplicate theorem name " ^ quote s
@@ -1166,7 +1166,7 @@
cd cwd;
if cwd subdir_of (!base_path) then ()
- else writeln "Warning: The current working directory seems to be no \
+ else warning "The current working directory seems to be no \
\subdirectory of\nIsabelle's main directory. \
\Please ensure that base_path's value is correct.\n";
--- a/src/Pure/goals.ML Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/goals.ML Fri Mar 15 12:01:19 1996 +0100
@@ -311,9 +311,9 @@
None => error"by: tactic failed"
| Some(th2,ths2) =>
(if eq_thm(th,th2)
- then writeln"Warning: same as previous level"
+ then warning "same as previous level"
else if eq_thm_sg(th,th2) then ()
- else writeln("Warning: signature of proof state has changed" ^
+ else warning("signature of proof state has changed" ^
sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
((th2,ths2)::(th,ths)::pairs)));
@@ -333,9 +333,9 @@
None => (writeln"Going back a level..."; backtrack pairs)
| Some(th2,thstr2) =>
(if eq_thm(th,th2)
- then writeln"Warning: same as previous choice at this level"
+ then warning "same as previous choice at this level"
else if eq_thm_sg(th,th2) then ()
- else writeln"Warning: signature of proof state has changed";
+ else warning "signature of proof state has changed";
(th2,thstr2)::pairs));
fun back() = setstate (backtrack (getstate()));
--- a/src/Pure/library.ML Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/library.ML Fri Mar 15 12:01:19 1996 +0100
@@ -703,14 +703,22 @@
(** input / output **)
-fun prs s = output (std_out, s);
+val prs_fn = ref(fn s => output (std_out, s));
+
+fun prs s = !prs_fn s;
fun writeln s = prs (s ^ "\n");
+(*print warning*)
+val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
+fun warning s = !warning_fn ("Warning: " ^ s);
(*print error message and abort to top level*)
+
+val error_fn = ref(fn s => output (std_out, s ^ "\n"));
+
exception ERROR;
-fun error msg = (writeln msg; raise ERROR);
-fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
+fun error msg = (!error_fn msg; raise ERROR);
+fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
fun assert p msg = if p then () else error msg;
fun deny p msg = if p then error msg else ();
--- a/src/Pure/sign.ML Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/sign.ML Fri Mar 15 12:01:19 1996 +0100
@@ -315,7 +315,7 @@
fun warn() =
if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
then (*no warning shown yet*)
- writeln "Warning: Currently parsed input \
+ warning "Currently parsed input \
\produces more than one parse tree.\n\
\For more information lower Syntax.ambiguity_level."
else ();
--- a/src/Pure/thm.ML Thu Mar 14 16:40:18 1996 +0100
+++ b/src/Pure/thm.ML Fri Mar 15 12:01:19 1996 +0100
@@ -1353,12 +1353,18 @@
fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t));
+fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t));
+
val trace_simp = ref false;
fun trace_term a sign t = if !trace_simp then prtm a sign t else ();
fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
+fun trace_term_warning a sign t = if !trace_simp then prtm_warning a sign t else ();
+
+fun trace_thm_warning a (Thm{sign,prop,...}) = trace_term_warning a sign prop;
+
fun vperm(Var _, Var _) = true
| vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t)
| vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2)
@@ -1395,7 +1401,7 @@
andalso not(is_Var(elhs))
in
if not perm andalso loops sign prems (elhs,erhs) then
- (prtm "Warning: ignoring looping rewrite rule" sign prop; None)
+ (prtm_warning "ignoring looping rewrite rule" sign prop; None)
else Some{thm=thm,lhs=lhs,perm=perm}
end;
@@ -1412,7 +1418,7 @@
(trace_thm "Adding rewrite rule:" thm;
Mss{net = (Net.insert_term((lhs,rrule),net,eq)
handle Net.INSERT =>
- (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
+ (prtm_warning "ignoring duplicate rewrite rule" sign prop;
net)),
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews});
@@ -1423,7 +1429,7 @@
| Some(rrule as {lhs,...}) =>
Mss{net = (Net.delete_term((lhs,rrule),net,eq)
handle Net.INSERT =>
- (prtm "Warning: rewrite rule not in simpset" sign prop;
+ (prtm_warning "rewrite rule not in simpset" sign prop;
net)),
congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}
@@ -1543,7 +1549,7 @@
let val etat = Pattern.eta_contract t;
fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
let val unit = if Sign.subsig(sign,signt) then ()
- else (trace_thm"Warning: rewrite rule from different theory"
+ else (trace_thm_warning "rewrite rule from different theory"
thm;
raise Pattern.MATCH)
val rprop = if maxidxt = ~1 then prop