src/Pure/ML/ml_compiler.ML
changeset 60956 10d463883dc2
parent 60858 7bf2188a0998
child 62357 ab76bd43c14a
equal deleted inserted replaced
60955:65149ae760a0 60956:10d463883dc2
     6 
     6 
     7 signature ML_COMPILER =
     7 signature ML_COMPILER =
     8 sig
     8 sig
     9   type flags =
     9   type flags =
    10     {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    10     {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    11       writeln: string -> unit, warning: string -> unit}
    11       debug: bool option, writeln: string -> unit, warning: string -> unit}
    12   val flags: flags
    12   val flags: flags
    13   val verbose: bool -> flags -> flags
    13   val verbose: bool -> flags -> flags
    14   val eval: flags -> Position.T -> ML_Lex.token list -> unit
    14   val eval: flags -> Position.T -> ML_Lex.token list -> unit
    15 end
    15 end
    16 
    16 
    17 structure ML_Compiler: ML_COMPILER =
    17 structure ML_Compiler: ML_COMPILER =
    18 struct
    18 struct
    19 
    19 
    20 type flags =
    20 type flags =
    21   {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    21   {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    22     writeln: string -> unit, warning: string -> unit};
    22     debug: bool option, writeln: string -> unit, warning: string -> unit};
    23 
    23 
    24 val flags: flags =
    24 val flags: flags =
    25   {SML = false, exchange = false, redirect = false, verbose = false,
    25   {SML = false, exchange = false, redirect = false, verbose = false,
    26     writeln = writeln, warning = warning};
    26     debug = NONE, writeln = writeln, warning = warning};
    27 
    27 
    28 fun verbose b (flags: flags) =
    28 fun verbose b (flags: flags) =
    29   {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
    29   {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
    30     writeln = #writeln flags, warning = #warning flags};
    30     verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
    31 
    31 
    32 fun eval (flags: flags) pos toks =
    32 fun eval (flags: flags) pos toks =
    33   let
    33   let
    34     val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
    34     val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
    35     val line = the_default 1 (Position.line_of pos);
    35     val line = the_default 1 (Position.line_of pos);
    36     val file = the_default "ML" (Position.file_of pos);
    36     val file = the_default "ML" (Position.file_of pos);
       
    37     val debug = the_default false (#debug flags);
    37     val text = ML_Lex.flatten toks;
    38     val text = ML_Lex.flatten toks;
    38   in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end;
    39   in
       
    40     Secure.use_text ML_Env.local_context
       
    41       {line = line, file = file, verbose = #verbose flags, debug = debug} text
       
    42   end;
    39 
    43 
    40 end;
    44 end;
    41