src/Pure/RAW/compiler_polyml.ML
changeset 62490 39d01eaf5292
parent 62489 36f11bc393a2
child 62493 dd154240a53c
equal deleted inserted replaced
62489:36f11bc393a2 62490:39d01eaf5292
     1 (*  Title:      Pure/RAW/compiler_polyml.ML
     1 (*  Title:      Pure/RAW/compiler_polyml.ML
     2 
     2 
     3 Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
     3 Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
     4 *)
     4 *)
     5 
     5 
       
     6 type use_context =
       
     7  {name_space: ML_Name_Space.T,
       
     8   str_of_pos: int -> string -> string,
       
     9   print: string -> unit,
       
    10   error: string -> unit};
       
    11 
     6 local
    12 local
       
    13 
       
    14 val boot_context: use_context =
       
    15  {name_space = ML_Name_Space.global,
       
    16   str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
       
    17   print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
       
    18   error = fn s => raise Fail s};
     7 
    19 
     8 fun drop_newline s =
    20 fun drop_newline s =
     9   if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    21   if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    10   else s;
    22   else s;
    11 
    23 
    53   let
    65   let
    54     val instream = TextIO.openIn file;
    66     val instream = TextIO.openIn file;
    55     val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    67     val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    56   in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    68   in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    57 
    69 
    58 fun use file =
    70 
    59   use_file boot_context {verbose = true, debug = false} file
    71 fun use_debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
       
    72   | use_debug_option (SOME debug) = debug;
       
    73 
       
    74 local
       
    75 
       
    76 fun use_ opt_debug file =
       
    77   use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file
    60     handle Fail msg => (#print boot_context msg; raise Fail "ML error");
    78     handle Fail msg => (#print boot_context msg; raise Fail "ML error");
    61 
    79 
       
    80 in
       
    81 
       
    82 val use = use_ NONE;
       
    83 val use_debug = use_ (SOME true);
       
    84 val use_no_debug = use_ (SOME false);
       
    85 
    62 end;
    86 end;
       
    87 
       
    88 end;