use_text: added name argument;
authorwenzelm
Sun Jan 21 16:43:42 2007 +0100 (2007-01-21)
changeset 22144c33450acd873
parent 22143 cf58486ca11b
child 22145 fedad292f738
use_text: added name argument;
src/Pure/General/secure.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml-5.0.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/poplogml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/Thy/thm_database.ML
src/Pure/Tools/am_compiler.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/nbe.ML
src/Pure/codegen.ML
     1.1 --- a/src/Pure/General/secure.ML	Sun Jan 21 13:27:41 2007 +0100
     1.2 +++ b/src/Pure/General/secure.ML	Sun Jan 21 16:43:42 2007 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4    val set_secure: unit -> unit
     1.5    val is_secure: unit -> bool
     1.6    val deny_secure: string -> unit
     1.7 -  val use_text: (string -> unit) * (string -> 'a) -> bool -> string -> unit
     1.8 +  val use_text: string -> (string -> unit) * (string -> 'a) -> bool -> string -> unit
     1.9    val use_file: (string -> unit) * (string -> 'a) -> bool -> string -> unit
    1.10    val use: string -> unit
    1.11    val commit: unit -> unit
    1.12 @@ -40,12 +40,12 @@
    1.13  val orig_use_text = use_text;
    1.14  val orig_use_file = use_file;
    1.15  
    1.16 -fun use_text pr verbose txt = (secure_mltext (); orig_use_text pr verbose txt);
    1.17 +fun use_text name pr verbose txt = (secure_mltext (); orig_use_text name pr verbose txt);
    1.18  fun use_file pr verbose name = (secure_mltext (); orig_use_file pr verbose name);
    1.19  val use = use_file Output.ml_output true;
    1.20  
    1.21  (*commit is dynamically bound!*)
    1.22 -fun commit () = orig_use_text Output.ml_output false "commit();";
    1.23 +fun commit () = orig_use_text "" Output.ml_output false "commit();";
    1.24  
    1.25  
    1.26  (* shell commands *)
     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Sun Jan 21 13:27:41 2007 +0100
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Sun Jan 21 16:43:42 2007 +0100
     2.3 @@ -133,7 +133,7 @@
     2.4  (* ML command execution *)
     2.5  
     2.6  (*Can one redirect 'use' directly to an instream?*)
     2.7 -fun use_text _ _ txt =
     2.8 +fun use_text _ _ _ txt =
     2.9    let
    2.10      val tmp_name = FileSys.tmpName ();
    2.11      val tmp_file = TextIO.openOut tmp_name;
     3.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Sun Jan 21 13:27:41 2007 +0100
     3.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML	Sun Jan 21 16:43:42 2007 +0100
     3.3 @@ -12,9 +12,7 @@
     3.4  
     3.5  (* improved versions of use_text/file *)
     3.6  
     3.7 -local
     3.8 -
     3.9 -fun use_ml name (print, err) verbose txt =
    3.10 +fun use_text name (print, err) verbose txt =
    3.11    let
    3.12      val in_buffer = ref (explode txt);
    3.13      val out_buffer = ref ([]: string list);
    3.14 @@ -37,14 +35,8 @@
    3.15      if verbose then print (output ()) else ()
    3.16    end;
    3.17  
    3.18 -in
    3.19 -
    3.20 -fun use_text output = use_ml "ML text" output;
    3.21 -
    3.22  fun use_file output verbose name =
    3.23    let
    3.24      val instream = TextIO.openIn name;
    3.25      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    3.26 -  in use_ml name output verbose txt end;
    3.27 -
    3.28 -end;
    3.29 +  in use_text name output verbose txt end;
     4.1 --- a/src/Pure/ML-Systems/polyml.ML	Sun Jan 21 13:27:41 2007 +0100
     4.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sun Jan 21 16:43:42 2007 +0100
     4.3 @@ -90,7 +90,7 @@
     4.4  
     4.5  (* ML command execution -- 'eval' *)
     4.6  
     4.7 -fun use_text (print, err) verbose txt =
     4.8 +fun use_text name (print, err) verbose txt =
     4.9    let
    4.10      val in_buffer = ref (explode txt);
    4.11      val out_buffer = ref ([]: string list);
    4.12 @@ -107,7 +107,8 @@
    4.13          [] => ()
    4.14        | _ => (PolyML.compiler (get, put) (); exec ()));
    4.15    in
    4.16 -    exec () handle exn => (err (output ()); raise exn);
    4.17 +    exec () handle exn =>
    4.18 +      (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    4.19      if verbose then print (output ()) else ()
    4.20    end;
    4.21  
    4.22 @@ -119,7 +120,7 @@
    4.23    fun println s =
    4.24      (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut);
    4.25    fun eval "-q" = ()
    4.26 -    | eval txt = use_text (println, println) false txt;
    4.27 +    | eval txt = use_text "" (println, println) false txt;
    4.28  in
    4.29    val _ = PolyML.onEntry (fn () => app eval (CommandLine.arguments ()));
    4.30  end;
     5.1 --- a/src/Pure/ML-Systems/poplogml.ML	Sun Jan 21 13:27:41 2007 +0100
     5.2 +++ b/src/Pure/ML-Systems/poplogml.ML	Sun Jan 21 16:43:42 2007 +0100
     5.3 @@ -377,5 +377,5 @@
     5.4  
     5.5  end;
     5.6  
     5.7 -fun use_text _ _ txt = use_string txt;
     5.8 +fun use_text _ _ _ txt = use_string txt;
     5.9  fun use_file _ _ name = use name;
     6.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sun Jan 21 13:27:41 2007 +0100
     6.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sun Jan 21 16:43:42 2007 +0100
     6.3 @@ -96,7 +96,7 @@
     6.4  
     6.5  (* ML command execution *)
     6.6  
     6.7 -fun use_text (print, err) verbose txt =
     6.8 +fun use_text name (print, err) verbose txt =
     6.9    let
    6.10      val ref out_orig = Control.Print.out;
    6.11  
    6.12 @@ -108,7 +108,8 @@
    6.13    in
    6.14      Control.Print.out := out;
    6.15      Backend.Interact.useStream (TextIO.openString txt) handle exn =>
    6.16 -      (Control.Print.out := out_orig; err (output ()); raise exn);
    6.17 +      (Control.Print.out := out_orig;
    6.18 +        err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
    6.19      Control.Print.out := out_orig;
    6.20      if verbose then print (output ()) else ()
    6.21    end;
     7.1 --- a/src/Pure/Thy/thm_database.ML	Sun Jan 21 13:27:41 2007 +0100
     7.2 +++ b/src/Pure/Thy/thm_database.ML	Sun Jan 21 16:43:42 2007 +0100
     7.3 @@ -46,7 +46,7 @@
     7.4    else if name = "" then true
     7.5    else (warning ("Cannot bind theorem(s) " ^ quote name ^ " as ML value"); true);
     7.6  
     7.7 -val use_text_verbose = use_text Output.ml_output true;
     7.8 +val use_text_verbose = use_text "" Output.ml_output true;
     7.9  
    7.10  fun ml_store_thm (name, thm) =
    7.11    let val thm' = store_thm (name, thm) in
     8.1 --- a/src/Pure/Tools/am_compiler.ML	Sun Jan 21 13:27:41 2007 +0100
     8.2 +++ b/src/Pure/Tools/am_compiler.ML	Sun Jan 21 16:43:42 2007 +0100
     8.3 @@ -216,7 +216,7 @@
     8.4  	    end
     8.5      in
     8.6  	compiled_rewriter := NONE;	
     8.7 -	use_text (K (), K ()) false (!buffer);
     8.8 +	use_text "" Output.ml_output false (!buffer);
     8.9  	case !compiled_rewriter of 
    8.10  	    NONE => raise (Compile "cannot communicate with compiled function")
    8.11  	  | SOME r => (compiled_rewriter := NONE; fn t => term_of_clos (r t))
     9.1 --- a/src/Pure/Tools/codegen_serializer.ML	Sun Jan 21 13:27:41 2007 +0100
     9.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Sun Jan 21 16:43:42 2007 +0100
     9.3 @@ -1024,7 +1024,7 @@
     9.4    let
     9.5      fun output_file file = File.write (Path.explode file) o code_output;
     9.6      val output_diag = writeln o code_output;
     9.7 -    val output_internal = use_text Output.ml_output false o code_output;
     9.8 +    val output_internal = use_text "" Output.ml_output false o code_output;
     9.9    in
    9.10      parse_args ((Args.$$$ "-" >> K output_diag
    9.11        || Args.$$$ "#" >> K output_internal
    9.12 @@ -1592,7 +1592,7 @@
    9.13      fun eval p = (
    9.14        reff := NONE;
    9.15        if !eval_verbose then Pretty.writeln p else ();
    9.16 -      use_text Output.ml_output (!eval_verbose)
    9.17 +      use_text "" Output.ml_output (!eval_verbose)
    9.18          ((Pretty.output o Pretty.chunks) [p,
    9.19            str ("val _ = (" ^ ref_name ^ " := SOME " ^ val_name' ^ ")")
    9.20          ]);
    10.1 --- a/src/Pure/Tools/nbe.ML	Sun Jan 21 13:27:41 2007 +0100
    10.2 +++ b/src/Pure/Tools/nbe.ML	Sun Jan 21 16:43:42 2007 +0100
    10.3 @@ -115,7 +115,7 @@
    10.4      fun use_code NONE = ()
    10.5        | use_code (SOME s) =
    10.6            (tracing (fn () => "\n---generated code:\n" ^ s) ();
    10.7 -           use_text (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
    10.8 +           use_text "" (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
    10.9                  Output.tracing o enclose "\n--- compiler echo (with error!):\n" "\n---\n")
   10.10              (!trace) s);
   10.11  
    11.1 --- a/src/Pure/codegen.ML	Sun Jan 21 13:27:41 2007 +0100
    11.2 +++ b/src/Pure/codegen.ML	Sun Jan 21 16:43:42 2007 +0100
    11.3 @@ -991,7 +991,7 @@
    11.4                    [Pretty.str "]"])]],
    11.5              Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
    11.6        "\n\nend;\n") ();
    11.7 -    val _ = use_text Output.ml_output false s;
    11.8 +    val _ = use_text "" Output.ml_output false s;
    11.9      fun iter f k = if k > i then NONE
   11.10        else (case (f () handle Match =>
   11.11            (warning "Exception Match raised in generated code"; NONE)) of
   11.12 @@ -1043,7 +1043,7 @@
   11.13              [Pretty.str "result"],
   11.14            Pretty.str ";"])  ^
   11.15        "\n\nend;\n";
   11.16 -    val _ = use_text Output.ml_output false s
   11.17 +    val _ = use_text "" Output.ml_output false s
   11.18    in !eval_result end);
   11.19  
   11.20  fun print_evaluated_term s = Toplevel.keep (fn state =>
   11.21 @@ -1150,7 +1150,7 @@
   11.22         val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
   11.23         val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs
   11.24       in ((case opt_fname of
   11.25 -         NONE => use_text Output.ml_output false
   11.26 +         NONE => use_text "" Output.ml_output false
   11.27             (space_implode "\n" (map snd code))
   11.28         | SOME fname =>
   11.29             if lib then