# HG changeset patch # User berghofe # Date 826887679 -3600 # Node ID e3fd931e60958abc226ea939c3868f371b91cc4b # Parent 688e18023915ac75f0396fea72acb2372a019e4a Added some functions which allow redirection of Isabelle's output diff -r 688e18023915 -r e3fd931e6095 src/Pure/Syntax/parser.ML --- 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 (); diff -r 688e18023915 -r e3fd931e6095 src/Pure/Syntax/syntax.ML --- 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 (); diff -r 688e18023915 -r e3fd931e6095 src/Pure/Thy/thm_database.ML --- 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 diff -r 688e18023915 -r e3fd931e6095 src/Pure/Thy/thy_read.ML --- 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"; diff -r 688e18023915 -r e3fd931e6095 src/Pure/goals.ML --- 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())); diff -r 688e18023915 -r e3fd931e6095 src/Pure/library.ML --- 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 (); diff -r 688e18023915 -r e3fd931e6095 src/Pure/sign.ML --- 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 (); diff -r 688e18023915 -r e3fd931e6095 src/Pure/thm.ML --- 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