src/Pure/ML/ml_context.ML
changeset 56275 600f432ab556
parent 56229 f61eaab6bec3
child 56278 2576d3a40ed6
     1.1 --- a/src/Pure/ML/ml_context.ML	Tue Mar 25 10:37:10 2014 +0100
     1.2 +++ b/src/Pure/ML/ml_context.ML	Tue Mar 25 13:18:10 2014 +0100
     1.3 @@ -21,12 +21,12 @@
     1.4    val trace: bool Config.T
     1.5    val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     1.6      Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
     1.7 -  val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
     1.8 -  val eval_file: bool -> Path.T -> unit
     1.9 -  val eval_source: bool -> Symbol_Pos.source -> unit
    1.10 -  val eval_in: Proof.context option -> bool -> Position.T ->
    1.11 +  val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
    1.12 +  val eval_file: ML_Compiler.flags -> Path.T -> unit
    1.13 +  val eval_source: ML_Compiler.flags -> Symbol_Pos.source -> unit
    1.14 +  val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
    1.15      ML_Lex.token Antiquote.antiquote list -> unit
    1.16 -  val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> unit
    1.17 +  val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
    1.18    val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
    1.19      Context.generic -> Context.generic
    1.20  end
    1.21 @@ -140,8 +140,10 @@
    1.22  val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
    1.23  val trace = Config.bool trace_raw;
    1.24  
    1.25 -fun eval verbose pos ants =
    1.26 +fun eval flags pos ants =
    1.27    let
    1.28 +    val non_verbose = {SML = #SML flags, verbose = false};
    1.29 +
    1.30      (*prepare source text*)
    1.31      val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
    1.32      val _ =
    1.33 @@ -157,11 +159,11 @@
    1.34      val _ =
    1.35        Context.setmp_thread_data
    1.36          (Option.map (Context.mapping I (Context_Position.set_visible false)) env_ctxt)
    1.37 -        (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) ()
    1.38 +        (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
    1.39        |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
    1.40  
    1.41 -    val _ = ML_Compiler.eval verbose pos body;
    1.42 -    val _ = ML_Compiler.eval false Position.none reset_env;
    1.43 +    val _ = ML_Compiler.eval flags pos body;
    1.44 +    val _ = ML_Compiler.eval non_verbose Position.none reset_env;
    1.45    in () end;
    1.46  
    1.47  end;
    1.48 @@ -169,29 +171,29 @@
    1.49  
    1.50  (* derived versions *)
    1.51  
    1.52 -fun eval_file verbose path =
    1.53 +fun eval_file flags path =
    1.54    let val pos = Path.position path
    1.55 -  in eval verbose pos (ML_Lex.read pos (File.read path)) end;
    1.56 +  in eval flags pos (ML_Lex.read pos (File.read path)) end;
    1.57  
    1.58 -fun eval_source verbose source =
    1.59 -  eval verbose (#pos source) (ML_Lex.read_source source);
    1.60 +fun eval_source flags source =
    1.61 +  eval flags (#pos source) (ML_Lex.read_source source);
    1.62  
    1.63 -fun eval_in ctxt verbose pos ants =
    1.64 +fun eval_in ctxt flags pos ants =
    1.65    Context.setmp_thread_data (Option.map Context.Proof ctxt)
    1.66 -    (fn () => eval verbose pos ants) ();
    1.67 +    (fn () => eval flags pos ants) ();
    1.68  
    1.69 -fun eval_source_in ctxt verbose source =
    1.70 +fun eval_source_in ctxt flags source =
    1.71    Context.setmp_thread_data (Option.map Context.Proof ctxt)
    1.72 -    (fn () => eval_source verbose source) ();
    1.73 +    (fn () => eval_source flags source) ();
    1.74  
    1.75  fun expression pos bind body ants =
    1.76 -  exec (fn () => eval false pos
    1.77 +  exec (fn () => eval {SML = false, verbose = false} pos
    1.78      (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
    1.79        ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
    1.80  
    1.81  end;
    1.82  
    1.83  fun use s =
    1.84 -  ML_Context.eval_file true (Path.explode s)
    1.85 +  ML_Context.eval_file {SML = false, verbose = true} (Path.explode s)
    1.86      handle ERROR msg => (writeln msg; error "ML error");
    1.87