updated use_text/file for 5.2;
authorwenzelm
Mon Mar 24 18:35:43 2008 +0100 (2008-03-24 ago)
changeset 26379a01a05cdd3b8
parent 26378 bac8d5e5f833
child 26380 5d368eb42c11
updated use_text/file for 5.2;
src/Pure/ML-Systems/polyml.ML
     1.1 --- a/src/Pure/ML-Systems/polyml.ML	Mon Mar 24 18:35:42 2008 +0100
     1.2 +++ b/src/Pure/ML-Systems/polyml.ML	Mon Mar 24 18:35:43 2008 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/ML-Systems/polyml.ML
     1.5      ID:         $Id$
     1.6  
     1.7 -Compatibility wrapper for Poly/ML 5.1/5.2.
     1.8 +Compatibility wrapper for Poly/ML (after 5.1).
     1.9  *)
    1.10  
    1.11  use "ML-Systems/polyml_common.ML";
    1.12 @@ -24,7 +24,7 @@
    1.13  
    1.14  fun use_text (tune: string -> string) name (print, err) verbose txt =
    1.15    let
    1.16 -    val in_buffer = ref (explode (tune txt));
    1.17 +    val in_buffer = ref (String.explode (tune txt));
    1.18      val out_buffer = ref ([]: string list);
    1.19      fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.20  
    1.21 @@ -32,16 +32,17 @@
    1.22      fun line () = ! line_no;
    1.23      fun get () =
    1.24        (case ! in_buffer of
    1.25 -        [] => ""
    1.26 -      | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
    1.27 +        [] => NONE
    1.28 +      | c :: cs => (in_buffer := cs; if c = #"\n" then line_no := ! line_no + 1 else (); SOME c));
    1.29      fun put s = out_buffer := s :: ! out_buffer;
    1.30  
    1.31 -    fun exec () =
    1.32 -      (case ! in_buffer of
    1.33 -        [] => ()
    1.34 -      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
    1.35 +    val _ =
    1.36 +      (while not (List.null (! in_buffer)) do
    1.37 +        PolyML.compiler
    1.38 +          {getChar = get, putString = put, lineNumber = line, fileName = name,
    1.39 +            nameSpace = PolyML.globalNameSpace} ())
    1.40 +      handle exn => (err (output ()); raise exn);
    1.41    in
    1.42 -    exec () handle exn => (err (output ()); raise exn);
    1.43      if verbose then print (output ()) else ()
    1.44    end;
    1.45  
    1.46 @@ -50,3 +51,4 @@
    1.47      val instream = TextIO.openIn name;
    1.48      val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.49    in use_text tune name output verbose txt end;
    1.50 +