Added some functions which allow redirection of Isabelle's output
authorberghofe
Fri Mar 15 12:01:19 1996 +0100 (1996-03-15)
changeset 1580e3fd931e6095
parent 1579 688e18023915
child 1581 a82618a900e5
Added some functions which allow redirection of Isabelle's output
src/Pure/Syntax/parser.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/thm_database.ML
src/Pure/Thy/thy_read.ML
src/Pure/goals.ML
src/Pure/library.ML
src/Pure/sign.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Syntax/parser.ML	Thu Mar 14 16:40:18 1996 +0100
     1.2 +++ b/src/Pure/Syntax/parser.ML	Fri Mar 15 12:01:19 1996 +0100
     1.3 @@ -752,7 +752,7 @@
     1.4              val dummy =
     1.5                if not (!warned) andalso
     1.6                   length (new_states @ States) > (!branching_level) then
     1.7 -                (writeln "Warning: Currently parsed expression could be \
     1.8 +                (warning "Currently parsed expression could be \
     1.9                           \extremely ambiguous.";
    1.10                   warned := true)
    1.11                else ();
     2.1 --- a/src/Pure/Syntax/syntax.ML	Thu Mar 14 16:40:18 1996 +0100
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Mar 15 12:01:19 1996 +0100
     2.3 @@ -308,7 +308,7 @@
     2.4      fun show_pt pt = writeln (str_of_ast (pt_to_ast (K None) pt));
     2.5    in
     2.6      if length pts > ! ambiguity_level then
     2.7 -      (writeln ("Warning: Ambiguous input " ^ quote str);
     2.8 +      (warning ("Ambiguous input " ^ quote str);
     2.9         writeln "produces the following parse trees:";
    2.10         seq show_pt pts)
    2.11      else ();
     3.1 --- a/src/Pure/Thy/thm_database.ML	Thu Mar 14 16:40:18 1996 +0100
     3.2 +++ b/src/Pure/Thy/thm_database.ML	Fri Mar 15 12:01:19 1996 +0100
     3.3 @@ -86,7 +86,7 @@
     3.4              end;
     3.5  
     3.6        val const_idx' = update_db false consts const_idx;
     3.7 -  in if consts = [] then writeln ("Warning: Theorem " ^ name ^
     3.8 +  in if consts = [] then warning ("Theorem " ^ name ^
     3.9                                    " cannot be stored in ThmDB\n\t because it \
    3.10                                    \contains no or only ignored constants.")
    3.11       else if is_some const_idx' then
     4.1 --- a/src/Pure/Thy/thy_read.ML	Thu Mar 14 16:40:18 1996 +0100
     4.2 +++ b/src/Pure/Thy/thy_read.ML	Fri Mar 15 12:01:19 1996 +0100
     4.3 @@ -299,7 +299,7 @@
     4.4                                       else (find_file abs_path (name ^ ".thy"),
     4.5                                             find_file abs_path (name ^ ".ML"))
     4.6         in if thy_file = "" andalso ml_file = "" then
     4.7 -            (writeln ("Warning: File \"" ^ (tack_on path name)
     4.8 +            (warning ("File \"" ^ (tack_on path name)
     4.9                        ^ ".thy\"\ncontaining theory \"" ^ name
    4.10                        ^ "\" no longer exists.");
    4.11               new_filename ()
    4.12 @@ -543,7 +543,7 @@
    4.13        in mk_entry relatives end;
    4.14    in if is_some (!cur_htmlfile) then
    4.15         (close_out (the (!cur_htmlfile));
    4.16 -        writeln "Warning: Last theory's HTML file has not been closed.")
    4.17 +        warning "Last theory's HTML file has not been closed.")
    4.18       else ();
    4.19       cur_htmlfile := Some (open_out (tack_on tpath ("." ^ tname ^ ".html")));
    4.20       cur_has_title := false;
    4.21 @@ -668,7 +668,7 @@
    4.22                  val fname = tack_on path ("." ^ t ^ "_sub.html");
    4.23                  val out = if file_exists fname then
    4.24                              open_append fname  handle Io s =>
    4.25 -                              (writeln ("Warning: Unable to write to file ." ^
    4.26 +                              (warning ("Unable to write to file ." ^
    4.27                                          fname); raise Io s)
    4.28                            else raise MK_HTML;
    4.29              in output (out,
    4.30 @@ -1039,7 +1039,7 @@
    4.31      val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
    4.32        handle Symtab.DUPLICATE s => 
    4.33          (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
    4.34 -           (writeln ("Warning: Theory database already contains copy of\
    4.35 +           (warning ("Theory database already contains copy of\
    4.36                       \ theorem " ^ quote name);
    4.37              (thms, true))
    4.38           else error ("Duplicate theorem name " ^ quote s
    4.39 @@ -1166,7 +1166,7 @@
    4.40       cd cwd;
    4.41  
    4.42       if cwd subdir_of (!base_path) then ()
    4.43 -     else writeln "Warning: The current working directory seems to be no \
    4.44 +     else warning "The current working directory seems to be no \
    4.45                    \subdirectory of\nIsabelle's main directory. \
    4.46                    \Please ensure that base_path's value is correct.\n";
    4.47  
     5.1 --- a/src/Pure/goals.ML	Thu Mar 14 16:40:18 1996 +0100
     5.2 +++ b/src/Pure/goals.ML	Fri Mar 15 12:01:19 1996 +0100
     5.3 @@ -311,9 +311,9 @@
     5.4       None      => error"by: tactic failed"
     5.5     | Some(th2,ths2) => 
     5.6         (if eq_thm(th,th2) 
     5.7 -	  then writeln"Warning: same as previous level"
     5.8 +	  then warning "same as previous level"
     5.9  	  else if eq_thm_sg(th,th2) then ()
    5.10 -	  else writeln("Warning: signature of proof state has changed" ^
    5.11 +	  else warning("signature of proof state has changed" ^
    5.12  		       sign_error (#sign(rep_thm th), #sign(rep_thm th2)));
    5.13         ((th2,ths2)::(th,ths)::pairs)));
    5.14  
    5.15 @@ -333,9 +333,9 @@
    5.16  	  None      => (writeln"Going back a level..."; backtrack pairs)
    5.17  	| Some(th2,thstr2) =>  
    5.18  	   (if eq_thm(th,th2) 
    5.19 -	      then writeln"Warning: same as previous choice at this level"
    5.20 +	      then warning "same as previous choice at this level"
    5.21  	      else if eq_thm_sg(th,th2) then ()
    5.22 -	      else writeln"Warning: signature of proof state has changed";
    5.23 +	      else warning "signature of proof state has changed";
    5.24  	    (th2,thstr2)::pairs));
    5.25  
    5.26  fun back() = setstate (backtrack (getstate()));
     6.1 --- a/src/Pure/library.ML	Thu Mar 14 16:40:18 1996 +0100
     6.2 +++ b/src/Pure/library.ML	Fri Mar 15 12:01:19 1996 +0100
     6.3 @@ -703,14 +703,22 @@
     6.4  
     6.5  (** input / output **)
     6.6  
     6.7 -fun prs s = output (std_out, s);
     6.8 +val prs_fn = ref(fn s => output (std_out, s));
     6.9 +
    6.10 +fun prs s = !prs_fn s;
    6.11  fun writeln s = prs (s ^ "\n");
    6.12  
    6.13 +(*print warning*)
    6.14 +val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
    6.15 +fun warning s = !warning_fn ("Warning: " ^ s);
    6.16  
    6.17  (*print error message and abort to top level*)
    6.18 +
    6.19 +val error_fn = ref(fn s => output (std_out, s ^ "\n"));
    6.20 +
    6.21  exception ERROR;
    6.22 -fun error msg = (writeln msg; raise ERROR);
    6.23 -fun sys_error msg = (writeln "*** SYSTEM ERROR ***"; error msg);
    6.24 +fun error msg = (!error_fn msg; raise ERROR);
    6.25 +fun sys_error msg = (!error_fn "*** SYSTEM ERROR ***"; error msg);
    6.26  
    6.27  fun assert p msg = if p then () else error msg;
    6.28  fun deny p msg = if p then error msg else ();
     7.1 --- a/src/Pure/sign.ML	Thu Mar 14 16:40:18 1996 +0100
     7.2 +++ b/src/Pure/sign.ML	Fri Mar 15 12:01:19 1996 +0100
     7.3 @@ -315,7 +315,7 @@
     7.4      fun warn() =
     7.5        if length ts > 1 andalso length ts <= !Syntax.ambiguity_level
     7.6        then (*no warning shown yet*)
     7.7 -           writeln "Warning: Currently parsed input \
     7.8 +           warning "Currently parsed input \
     7.9                     \produces more than one parse tree.\n\
    7.10                     \For more information lower Syntax.ambiguity_level."
    7.11        else ();
     8.1 --- a/src/Pure/thm.ML	Thu Mar 14 16:40:18 1996 +0100
     8.2 +++ b/src/Pure/thm.ML	Fri Mar 15 12:01:19 1996 +0100
     8.3 @@ -1353,12 +1353,18 @@
     8.4  
     8.5  fun prtm a sign t = (writeln a; writeln(Sign.string_of_term sign t));
     8.6  
     8.7 +fun prtm_warning a sign t = warning (a ^ "\n" ^ (Sign.string_of_term sign t));
     8.8 +
     8.9  val trace_simp = ref false;
    8.10  
    8.11  fun trace_term a sign t = if !trace_simp then prtm a sign t else ();
    8.12  
    8.13  fun trace_thm a (Thm{sign,prop,...}) = trace_term a sign prop;
    8.14  
    8.15 +fun trace_term_warning a sign t = if !trace_simp then prtm_warning a sign t else ();
    8.16 +
    8.17 +fun trace_thm_warning a (Thm{sign,prop,...}) = trace_term_warning a sign prop;
    8.18 +
    8.19  fun vperm(Var _, Var _) = true
    8.20    | vperm(Abs(_,_,s), Abs(_,_,t)) = vperm(s,t)
    8.21    | vperm(t1$t2, u1$u2) = vperm(t1,u1) andalso vperm(t2,u2)
    8.22 @@ -1395,7 +1401,7 @@
    8.23                                       andalso not(is_Var(elhs))
    8.24    in
    8.25       if not perm andalso loops sign prems (elhs,erhs) then
    8.26 -       (prtm "Warning: ignoring looping rewrite rule" sign prop; None)
    8.27 +       (prtm_warning "ignoring looping rewrite rule" sign prop; None)
    8.28       else Some{thm=thm,lhs=lhs,perm=perm}
    8.29    end;
    8.30  
    8.31 @@ -1412,7 +1418,7 @@
    8.32        (trace_thm "Adding rewrite rule:" thm;
    8.33         Mss{net = (Net.insert_term((lhs,rrule),net,eq)
    8.34                   handle Net.INSERT =>
    8.35 -                  (prtm "Warning: ignoring duplicate rewrite rule" sign prop;
    8.36 +                  (prtm_warning "ignoring duplicate rewrite rule" sign prop;
    8.37                     net)),
    8.38             congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews});
    8.39  
    8.40 @@ -1423,7 +1429,7 @@
    8.41    | Some(rrule as {lhs,...}) =>
    8.42        Mss{net = (Net.delete_term((lhs,rrule),net,eq)
    8.43                  handle Net.INSERT =>
    8.44 -                 (prtm "Warning: rewrite rule not in simpset" sign prop;
    8.45 +                 (prtm_warning "rewrite rule not in simpset" sign prop;
    8.46                    net)),
    8.47               congs=congs, bounds=bounds, prems=prems,mk_rews=mk_rews}
    8.48  
    8.49 @@ -1543,7 +1549,7 @@
    8.50    let val etat = Pattern.eta_contract t;
    8.51        fun rew {thm as Thm{sign,der,maxidx,shyps,hyps,prop,...}, lhs, perm} =
    8.52          let val unit = if Sign.subsig(sign,signt) then ()
    8.53 -                  else (trace_thm"Warning: rewrite rule from different theory"
    8.54 +                  else (trace_thm_warning "rewrite rule from different theory"
    8.55                            thm;
    8.56                          raise Pattern.MATCH)
    8.57              val rprop = if maxidxt = ~1 then prop