src/Pure/ML/ml_compiler.ML
changeset 56618 874bdedb2313
parent 56304 40274e4f5ebf
child 60858 7bf2188a0998
     1.1 --- a/src/Pure/ML/ml_compiler.ML	Thu Apr 17 14:52:23 2014 +0200
     1.2 +++ b/src/Pure/ML/ml_compiler.ML	Sat Apr 19 17:23:05 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature ML_COMPILER =
     1.6  sig
     1.7 -  type flags = {SML: bool, redirect: bool, verbose: bool}
     1.8 +  type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool}
     1.9    val flags: flags
    1.10    val verbose: bool -> flags -> flags
    1.11    val eval: flags -> Position.T -> ML_Lex.token list -> unit
    1.12 @@ -15,9 +15,11 @@
    1.13  structure ML_Compiler: ML_COMPILER =
    1.14  struct
    1.15  
    1.16 -type flags = {SML: bool, redirect: bool, verbose: bool};
    1.17 -val flags = {SML = false, redirect = false, verbose = false};
    1.18 -fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v};
    1.19 +type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool};
    1.20 +val flags = {SML = false, exchange = false, redirect = false, verbose = false};
    1.21 +
    1.22 +fun verbose b (flags: flags) =
    1.23 +  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b};
    1.24  
    1.25  fun eval (flags: flags) pos toks =
    1.26    let