clarified environment: allow "read>write" specification;
authorwenzelm
Mon Aug 27 17:30:13 2018 +0200 (13 months ago)
changeset 688202e4df245754e
parent 68819 9cfa4aa35719
child 68821 877534be1930
clarified environment: allow "read>write" specification;
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_file.ML
src/Pure/Pure.thy
src/Pure/Tools/debugger.ML
     1.1 --- a/src/Pure/ML/ml_compiler.ML	Mon Aug 27 17:26:14 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 27 17:30:13 2018 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  signature ML_COMPILER =
     1.5  sig
     1.6    type flags =
     1.7 -    {read: string option, write: string option, redirect: bool, verbose: bool,
     1.8 +    {environment: string, redirect: bool, verbose: bool,
     1.9        debug: bool option, writeln: string -> unit, warning: string -> unit}
    1.10    val debug_flags: bool option -> flags
    1.11    val flags: flags
    1.12 @@ -21,17 +21,17 @@
    1.13  (* flags *)
    1.14  
    1.15  type flags =
    1.16 -  {read: string option, write: string option, redirect: bool, verbose: bool,
    1.17 +  {environment: string, redirect: bool, verbose: bool,
    1.18      debug: bool option, writeln: string -> unit, warning: string -> unit};
    1.19  
    1.20  fun debug_flags opt_debug : flags =
    1.21 -  {read = NONE, write = NONE, redirect = false, verbose = false,
    1.22 +  {environment = "", redirect = false, verbose = false,
    1.23      debug = opt_debug, writeln = writeln, warning = warning};
    1.24  
    1.25  val flags = debug_flags NONE;
    1.26  
    1.27  fun verbose b (flags: flags) =
    1.28 -  {read = #read flags, write = #write flags, redirect = #redirect flags, verbose = b,
    1.29 +  {environment = #environment flags, redirect = #redirect flags, verbose = b,
    1.30      debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
    1.31  
    1.32  
    1.33 @@ -154,15 +154,15 @@
    1.34      val opt_context = Context.get_generic_context ();
    1.35  
    1.36      val env as {debug, name_space, add_breakpoints} =
    1.37 -      (case (ML_Recursive.get (), is_some (#read flags) orelse is_some (#write flags)) of
    1.38 +      (case (ML_Recursive.get (), #environment flags <> "") of
    1.39          (SOME env, false) => env
    1.40        | _ =>
    1.41 -       {debug =
    1.42 -          (case #debug flags of
    1.43 -            SOME debug => debug
    1.44 -          | NONE => ML_Options.debugger_enabled opt_context),
    1.45 -        name_space = ML_Env.make_name_space {read = #read flags, write = #write flags},
    1.46 -        add_breakpoints = ML_Env.add_breakpoints});
    1.47 +         {debug =
    1.48 +            (case #debug flags of
    1.49 +              SOME debug => debug
    1.50 +            | NONE => ML_Options.debugger_enabled opt_context),
    1.51 +          name_space = ML_Env.make_name_space (#environment flags),
    1.52 +          add_breakpoints = ML_Env.add_breakpoints});
    1.53  
    1.54  
    1.55      (* input *)
    1.56 @@ -170,7 +170,8 @@
    1.57      val location_props = op ^ (YXML.output_markup (":", #props (Position.dest pos)));
    1.58  
    1.59      val input_explode =
    1.60 -      if ML_Env.is_standard (ML_Env.default_env (#read flags)) then String.explode
    1.61 +      if ML_Env.is_standard (#read (ML_Env.parse_environment opt_context (#environment flags)))
    1.62 +      then String.explode
    1.63        else maps (String.explode o Symbol.esc) o Symbol.explode;
    1.64  
    1.65      fun token_content tok =
     2.1 --- a/src/Pure/ML/ml_context.ML	Mon Aug 27 17:26:14 2018 +0200
     2.2 +++ b/src/Pure/ML/ml_context.ML	Mon Aug 27 17:30:13 2018 +0200
     2.3 @@ -195,8 +195,10 @@
     2.4    in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
     2.5  
     2.6  fun eval_source flags source =
     2.7 -  eval flags (Input.pos_of source)
     2.8 -    (ML_Lex.read_source (ML_Env.is_standard (ML_Env.default_env (#read flags))) source);
     2.9 +  let
    2.10 +    val opt_context = Context.get_generic_context ();
    2.11 +    val SML = ML_Env.is_standard (#read (ML_Env.parse_environment opt_context (#environment flags)));
    2.12 +  in eval flags (Input.pos_of source) (ML_Lex.read_source SML source) end;
    2.13  
    2.14  fun eval_in ctxt flags pos ants =
    2.15    Context.setmp_generic_context (Option.map Context.Proof ctxt)
     3.1 --- a/src/Pure/ML/ml_env.ML	Mon Aug 27 17:26:14 2018 +0200
     3.2 +++ b/src/Pure/ML/ml_env.ML	Mon Aug 27 17:30:13 2018 +0200
     3.3 @@ -19,12 +19,15 @@
     3.4    val ML_write_global: bool Config.T
     3.5    val inherit: Context.generic -> Context.generic -> Context.generic
     3.6    val setup: string -> theory -> theory
     3.7 -  val context_env: Context.generic -> string option -> string
     3.8 -  val default_env: string option -> string
     3.9 +  type environment = {read: string, write: string}
    3.10 +  val parse_environment: Context.generic option -> string -> environment
    3.11 +  val print_environment: environment -> string
    3.12 +  val SML_export: string
    3.13 +  val SML_import: string
    3.14    val forget_structure: string -> Context.generic -> Context.generic
    3.15    val bootstrap_name_space: Context.generic -> Context.generic
    3.16    val add_name_space: string -> ML_Name_Space.T -> Context.generic -> Context.generic
    3.17 -  val make_name_space: {read: string option, write: string option} -> ML_Name_Space.T
    3.18 +  val make_name_space: string -> ML_Name_Space.T
    3.19    val context: ML_Compiler0.context
    3.20    val name_space: ML_Name_Space.T
    3.21    val check_functor: string -> unit
    3.22 @@ -126,23 +129,36 @@
    3.23  
    3.24  (* environment name *)
    3.25  
    3.26 -fun check_env opt_context name =
    3.27 -  (case opt_context of
    3.28 -    NONE =>
    3.29 -      if name = Isabelle then name
    3.30 -      else error ("Bad ML environment name " ^ quote name ^ " -- no context")
    3.31 -  | SOME context => if name = Isabelle then name else (get_env context name; name));
    3.32 +type environment = {read: string, write: string};
    3.33 +
    3.34 +val separator = ">";
    3.35 +
    3.36 +fun parse_environment opt_context environment =
    3.37 +  let
    3.38 +    fun check name =
    3.39 +      (case opt_context of
    3.40 +        NONE =>
    3.41 +          if name = Isabelle then name
    3.42 +          else error ("Bad ML environment name " ^ quote name ^ " -- no context")
    3.43 +      | SOME context => if name = Isabelle then name else (get_env context name; name));
    3.44  
    3.45 -fun context_env context opt_name =
    3.46 -  check_env (SOME context) (the_default (Config.get_generic context ML_environment) opt_name);
    3.47 +    val spec =
    3.48 +      if environment = "" then
    3.49 +        (case opt_context of
    3.50 +          NONE => Isabelle
    3.51 +        | SOME context => Config.get_generic context ML_environment)
    3.52 +      else environment;
    3.53 +    val (read, write) =
    3.54 +      (case space_explode separator spec of
    3.55 +        [a] => (a, a)
    3.56 +      | [a, b] => (a, b)
    3.57 +      | _ => error ("Malformed ML environment specification: " ^ quote spec));
    3.58 +  in {read = check read, write = check write} end;
    3.59  
    3.60 -fun default_env opt_name =
    3.61 -  let val opt_context = Context.get_generic_context () in
    3.62 -    check_env opt_context
    3.63 -      (case opt_name of
    3.64 -        SOME name => name
    3.65 -      | NONE => (case opt_context of NONE => Isabelle | SOME context => context_env context NONE))
    3.66 -  end;
    3.67 +fun print_environment {read, write} = read ^ separator ^ write;
    3.68 +
    3.69 +val SML_export = print_environment {read = SML, write = Isabelle};
    3.70 +val SML_import = print_environment {read = Isabelle, write = SML};
    3.71  
    3.72  
    3.73  (* name space *)
    3.74 @@ -178,17 +194,16 @@
    3.75        val functor2 = fold Symtab.update (#allFunct space ()) functor1;
    3.76      in (val2, type2, fixity2, structure2, signature2, functor2) end);
    3.77  
    3.78 -fun make_name_space {read, write} : ML_Name_Space.T =
    3.79 +fun make_name_space environment : ML_Name_Space.T =
    3.80    let
    3.81 -    val read_env = default_env read;
    3.82 -    val write_env = default_env write;
    3.83 +    val {read, write} = parse_environment (Context.get_generic_context ()) environment;
    3.84  
    3.85 -    fun lookup_env sel1 context name = Symtab.lookup (sel1 (get_env context read_env)) name;
    3.86 -    fun dest_env sel1 context = Symtab.dest (sel1 (get_env context read_env));
    3.87 -    fun enter_env ap1 entry = update_env write_env (ap1 (Symtab.update entry));
    3.88 +    fun lookup_env sel1 context name = Symtab.lookup (sel1 (get_env context read)) name;
    3.89 +    fun dest_env sel1 context = Symtab.dest (sel1 (get_env context read));
    3.90 +    fun enter_env ap1 entry = update_env write (ap1 (Symtab.update entry));
    3.91  
    3.92      fun lookup sel1 sel2 name =
    3.93 -      if read_env = Isabelle then
    3.94 +      if read = Isabelle then
    3.95          (case Context.get_generic_context () of
    3.96            NONE => sel2 ML_Name_Space.global name
    3.97          | SOME context =>
    3.98 @@ -199,7 +214,7 @@
    3.99  
   3.100      fun all sel1 sel2 () =
   3.101        sort_distinct (string_ord o apply2 #1)
   3.102 -        (if read_env = Isabelle then
   3.103 +        (if read = Isabelle then
   3.104            (case Context.get_generic_context () of
   3.105              NONE => sel2 ML_Name_Space.global ()
   3.106            | SOME context =>
   3.107 @@ -208,7 +223,7 @@
   3.108           else dest_env sel1 (Context.the_generic_context ()));
   3.109  
   3.110      fun enter ap1 sel2 entry =
   3.111 -      if write_env = Isabelle then
   3.112 +      if write = Isabelle then
   3.113          (case Context.get_generic_context () of
   3.114            NONE => sel2 ML_Name_Space.global entry
   3.115          | SOME context =>
   3.116 @@ -237,7 +252,7 @@
   3.117    end;
   3.118  
   3.119  val context: ML_Compiler0.context =
   3.120 - {name_space = make_name_space {read = NONE, write = NONE},
   3.121 + {name_space = make_name_space "",
   3.122    print_depth = NONE,
   3.123    here = Position.here oo Position.line_file,
   3.124    print = writeln,
     4.1 --- a/src/Pure/ML/ml_file.ML	Mon Aug 27 17:26:14 2018 +0200
     4.2 +++ b/src/Pure/ML/ml_file.ML	Mon Aug 27 17:30:13 2018 +0200
     4.3 @@ -6,7 +6,7 @@
     4.4  
     4.5  signature ML_FILE =
     4.6  sig
     4.7 -  val command: string option -> bool option -> (theory -> Token.file list) ->
     4.8 +  val command: string -> bool option -> (theory -> Token.file list) ->
     4.9      Toplevel.transition -> Toplevel.transition
    4.10    val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    4.11    val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition
    4.12 @@ -15,7 +15,7 @@
    4.13  structure ML_File: ML_FILE =
    4.14  struct
    4.15  
    4.16 -fun command env debug files = Toplevel.generic_theory (fn gthy =>
    4.17 +fun command environment debug files = Toplevel.generic_theory (fn gthy =>
    4.18    let
    4.19      val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
    4.20      val provide = Resources.provide (src_path, digest);
    4.21 @@ -24,7 +24,7 @@
    4.22      val _ = Thy_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
    4.23  
    4.24      val flags: ML_Compiler.flags =
    4.25 -      {read = env, write = env, redirect = true, verbose = true,
    4.26 +      {environment = environment, redirect = true, verbose = true,
    4.27          debug = debug, writeln = writeln, warning = warning};
    4.28    in
    4.29      gthy
    4.30 @@ -33,7 +33,7 @@
    4.31      |> Context.mapping provide (Local_Theory.background_theory provide)
    4.32    end);
    4.33  
    4.34 -val ML = command NONE;
    4.35 -val SML = command (SOME ML_Env.SML);
    4.36 +val ML = command "";
    4.37 +val SML = command ML_Env.SML;
    4.38  
    4.39  end;
     5.1 --- a/src/Pure/Pure.thy	Mon Aug 27 17:26:14 2018 +0200
     5.2 +++ b/src/Pure/Pure.thy	Mon Aug 27 17:30:13 2018 +0200
     5.3 @@ -170,7 +170,7 @@
     5.4      (Parse.ML_source >> (fn source =>
     5.5        let
     5.6          val flags: ML_Compiler.flags =
     5.7 -          {read = SOME ML_Env.SML, write = NONE, redirect = false, verbose = true,
     5.8 +          {environment = ML_Env.SML_export, redirect = false, verbose = true,
     5.9              debug = NONE, writeln = writeln, warning = warning};
    5.10        in
    5.11          Toplevel.theory
    5.12 @@ -182,7 +182,7 @@
    5.13      (Parse.ML_source >> (fn source =>
    5.14        let
    5.15          val flags: ML_Compiler.flags =
    5.16 -          {read = NONE, write = SOME ML_Env.SML, redirect = false, verbose = true,
    5.17 +          {environment = ML_Env.SML_import, redirect = false, verbose = true,
    5.18              debug = NONE, writeln = writeln, warning = warning};
    5.19        in
    5.20          Toplevel.generic_theory
     6.1 --- a/src/Pure/Tools/debugger.ML	Mon Aug 27 17:26:14 2018 +0200
     6.2 +++ b/src/Pure/Tools/debugger.ML	Mon Aug 27 17:30:13 2018 +0200
     6.3 @@ -132,12 +132,10 @@
     6.4      "Context.put_generic_context (SOME ML_context)"];
     6.5  
     6.6  fun evaluate {SML, verbose} =
     6.7 -  let val env = ML_Env.make_standard SML in
     6.8 -    ML_Context.eval
     6.9 -      {read = SOME env, write = SOME env, redirect = false, verbose = verbose,
    6.10 -        debug = SOME false, writeln = writeln_message, warning = warning_message}
    6.11 -      Position.none
    6.12 -  end;
    6.13 +  ML_Context.eval
    6.14 +    {environment = ML_Env.make_standard SML, redirect = false, verbose = verbose,
    6.15 +      debug = SOME false, writeln = writeln_message, warning = warning_message}
    6.16 +    Position.none;
    6.17  
    6.18  fun eval_setup thread_name index SML context =
    6.19    context