# HG changeset patch
# User wenzelm
# Date 1397920985 -7200
# Node ID 874bdedb2313549b9b75a524c95296b2b0c6f070
# Parent  c006469967016e7d24e0fddfce961d69ec1608a7
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;

diff -r c00646996701 -r 874bdedb2313 NEWS
--- a/NEWS	Thu Apr 17 14:52:23 2014 +0200
+++ b/NEWS	Sat Apr 19 17:23:05 2014 +0200
@@ -37,11 +37,14 @@
 exception.  Potential INCOMPATIBILITY for non-conformant tactical
 proof tools.
 
-* Command 'SML_file' reads and evaluates the given Standard ML file.
+* Support for official Standard ML within the Isabelle context.
+Command 'SML_file' reads and evaluates the given Standard ML file.
 Toplevel bindings are stored within the theory context; the initial
 environment is restricted to the Standard ML implementation of
-Poly/ML, without the add-ons of Isabelle/ML.  See also
-~~/src/Tools/SML/Examples.thy for some basic examples.
+Poly/ML, without the add-ons of Isabelle/ML.  Commands 'SML_import'
+and 'SML_export' allow to exchange toplevel bindings between the two
+separate environments.  See also ~~/src/Tools/SML/Examples.thy for
+some examples.
 
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
diff -r c00646996701 -r 874bdedb2313 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Thu Apr 17 14:52:23 2014 +0200
+++ b/etc/isar-keywords-ZF.el	Sat Apr 19 17:23:05 2014 +0200
@@ -20,7 +20,9 @@
     "ProofGeneral\\.process_pgip"
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
+    "SML_export"
     "SML_file"
+    "SML_import"
     "abbreviation"
     "also"
     "apply"
@@ -345,7 +347,9 @@
 (defconst isar-keywords-theory-decl
   '("ML"
     "ML_file"
+    "SML_export"
     "SML_file"
+    "SML_import"
     "abbreviation"
     "attribute_setup"
     "axiomatization"
diff -r c00646996701 -r 874bdedb2313 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Apr 17 14:52:23 2014 +0200
+++ b/etc/isar-keywords.el	Sat Apr 19 17:23:05 2014 +0200
@@ -20,7 +20,9 @@
     "ProofGeneral\\.process_pgip"
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
+    "SML_export"
     "SML_file"
+    "SML_import"
     "abbreviation"
     "adhoc_overloading"
     "also"
@@ -483,7 +485,9 @@
 (defconst isar-keywords-theory-decl
   '("ML"
     "ML_file"
+    "SML_export"
     "SML_file"
+    "SML_import"
     "abbreviation"
     "adhoc_overloading"
     "atom_decl"
diff -r c00646996701 -r 874bdedb2313 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 19 17:23:05 2014 +0200
@@ -273,13 +273,30 @@
         let
           val ([{lines, pos, ...}], thy') = files thy;
           val source = {delimited = true, text = cat_lines lines, pos = pos};
-          val flags = {SML = true, redirect = true, verbose = true};
+          val flags = {SML = true, exchange = false, redirect = true, verbose = true};
         in
           thy' |> Context.theory_map
             (ML_Context.exec (fn () => ML_Context.eval_source flags source))
         end)));
 
 val _ =
+  Outer_Syntax.command @{command_spec "SML_export"} "evaluate SML within Isabelle/ML environment"
+    (Parse.ML_source >> (fn source =>
+      let val flags = {SML = true, exchange = true, redirect = false, verbose = true} in
+        Toplevel.theory
+          (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
+      end));
+
+val _ =
+  Outer_Syntax.command @{command_spec "SML_import"} "evaluate Isabelle/ML within SML environment"
+    (Parse.ML_source >> (fn source =>
+      let val flags = {SML = false, exchange = true, redirect = false, verbose = true} in
+        Toplevel.generic_theory
+          (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
+            Local_Theory.propagate_ml_env)
+      end));
+
+val _ =
   Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory
diff -r c00646996701 -r 874bdedb2313 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Sat Apr 19 17:23:05 2014 +0200
@@ -6,7 +6,7 @@
 
 signature ML_COMPILER =
 sig
-  type flags = {SML: bool, redirect: bool, verbose: bool}
+  type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool}
   val flags: flags
   val verbose: bool -> flags -> flags
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
@@ -15,9 +15,11 @@
 structure ML_Compiler: ML_COMPILER =
 struct
 
-type flags = {SML: bool, redirect: bool, verbose: bool};
-val flags = {SML = false, redirect = false, verbose = false};
-fun verbose v (flags: flags) = {SML = #SML flags, redirect = #redirect flags, verbose = v};
+type flags = {SML: bool, exchange: bool, redirect: bool, verbose: bool};
+val flags = {SML = false, exchange = false, redirect = false, verbose = false};
+
+fun verbose b (flags: flags) =
+  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b};
 
 fun eval (flags: flags) pos toks =
   let
diff -r c00646996701 -r 874bdedb2313 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Sat Apr 19 17:23:05 2014 +0200
@@ -70,7 +70,7 @@
 fun eval (flags: flags) pos toks =
   let
     val _ = Secure.secure_mltext ();
-    val space = if #SML flags then ML_Env.SML_name_space else ML_Env.name_space;
+    val space = ML_Env.name_space {SML = #SML flags, exchange = #exchange flags}
     val opt_context = Context.thread_data ();
 
 
diff -r c00646996701 -r 874bdedb2313 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/ML/ml_env.ML	Sat Apr 19 17:23:05 2014 +0200
@@ -8,9 +8,9 @@
 signature ML_ENV =
 sig
   val inherit: Context.generic -> Context.generic -> Context.generic
-  val SML_name_space: ML_Name_Space.T
-  val name_space: ML_Name_Space.T
+  val name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
   val local_context: use_context
+  val local_name_space: ML_Name_Space.T
   val check_functor: string -> unit
 end
 
@@ -64,62 +64,35 @@
 val inherit = Env.put o Env.get;
 
 
-(* SML name space *)
-
-val SML_name_space: ML_Name_Space.T =
-  let
-    fun lookup which name =
-      Context.the_thread_data ()
-      |> (fn context => Symtab.lookup (which (#sml_tables (Env.get context))) name);
-
-    fun all which () =
-      Context.the_thread_data ()
-      |> (fn context => Symtab.dest (which (#sml_tables (Env.get context))))
-      |> sort_distinct (string_ord o pairself #1);
+(* name space *)
 
-    fun enter which entry =
-      Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
-        let val sml_tables' = which (Symtab.update entry) sml_tables
-        in make_data (bootstrap, tables, sml_tables') end));
-  in
-   {lookupVal    = lookup #1,
-    lookupType   = lookup #2,
-    lookupFix    = lookup #3,
-    lookupStruct = lookup #4,
-    lookupSig    = lookup #5,
-    lookupFunct  = lookup #6,
-    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)),
-    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)),
-    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)),
-    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)),
-    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)),
-    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)),
-    allVal       = all #1,
-    allType      = all #2,
-    allFix       = all #3,
-    allStruct    = all #4,
-    allSig       = all #5,
-    allFunct     = all #6}
-  end;
-
-
-(* Isabelle/ML name space *)
-
-val name_space: ML_Name_Space.T =
+fun name_space {SML, exchange} : ML_Name_Space.T =
   let
     fun lookup sel1 sel2 name =
-      Context.thread_data ()
-      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
-      |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
+      if SML then
+        Context.the_thread_data ()
+        |> (fn context => Symtab.lookup (sel1 (#sml_tables (Env.get context))) name)
+      else
+        Context.thread_data ()
+        |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#tables (Env.get context))) name)
+        |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
 
     fun all sel1 sel2 () =
-      Context.thread_data ()
-      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
-      |> append (sel2 ML_Name_Space.global ())
+      (if SML then
+        Context.the_thread_data ()
+        |> (fn context => Symtab.dest (sel1 (#sml_tables (Env.get context))))
+      else
+        Context.thread_data ()
+        |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#tables (Env.get context))))
+        |> append (sel2 ML_Name_Space.global ()))
       |> sort_distinct (string_ord o pairself #1);
 
     fun enter ap1 sel2 entry =
-      if is_some (Context.thread_data ()) then
+      if SML <> exchange then
+        Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
+          let val sml_tables' = ap1 (Symtab.update entry) sml_tables
+          in make_data (bootstrap, tables, sml_tables') end))
+      else if is_some (Context.thread_data ()) then
         Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
           let
             val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
@@ -149,12 +122,14 @@
 
 val local_context: use_context =
  {tune_source = ML_Parse.fix_ints,
-  name_space = name_space,
+  name_space = name_space {SML = false, exchange = false},
   str_of_pos = Position.here oo Position.line_file,
   print = writeln,
   error = error};
 
-val is_functor = is_some o #lookupFunct name_space;
+val local_name_space = #name_space local_context;
+
+val is_functor = is_some o #lookupFunct local_name_space;
 
 fun check_functor name =
   if not (is_functor "Table") (*mask dummy version of name_space*) orelse is_functor name then ()
diff -r c00646996701 -r 874bdedb2313 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/Pure.thy	Sat Apr 19 17:23:05 2014 +0200
@@ -14,7 +14,6 @@
     "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
   and "theory" :: thy_begin % "theory"
-  and "SML_file" "ML_file" :: thy_load % "ML"
   and "header" :: diag
   and "chapter" :: thy_heading1
   and "section" :: thy_heading2
@@ -30,6 +29,8 @@
     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     "no_notation" "axiomatization" "theorems" "lemmas" "declare"
     "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
+  and "SML_file" "ML_file" :: thy_load % "ML"
+  and "SML_import" "SML_export" :: thy_decl % "ML"
   and "ML" :: thy_decl % "ML"
   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
   and "ML_val" "ML_command" :: diag % "ML"
diff -r c00646996701 -r 874bdedb2313 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Pure/pure_syn.ML	Sat Apr 19 17:23:05 2014 +0200
@@ -23,7 +23,7 @@
           val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
           val provide = Resources.provide (src_path, digest);
           val source = {delimited = true, text = cat_lines lines, pos = pos};
-          val flags = {SML = false, redirect = true, verbose = true};
+          val flags = {SML = false, exchange = false, redirect = true, verbose = true};
         in
           gthy
           |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
diff -r c00646996701 -r 874bdedb2313 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML	Sat Apr 19 17:23:05 2014 +0200
@@ -392,7 +392,7 @@
 
 fun notify_val (string, value) = 
   let
-    val _ = #enterVal ML_Env.name_space (string, value);
+    val _ = #enterVal ML_Env.local_name_space (string, value);
     val _ = Theory.setup (Loaded_Values.map (insert (op =) string));
   in () end;
 
@@ -401,24 +401,24 @@
 val notifying_context : use_context =
  {tune_source = #tune_source ML_Env.local_context,
   name_space =
-   {lookupVal    = #lookupVal ML_Env.name_space,
-    lookupType   = #lookupType ML_Env.name_space,
-    lookupFix    = #lookupFix ML_Env.name_space,
-    lookupStruct = #lookupStruct ML_Env.name_space,
-    lookupSig    = #lookupSig ML_Env.name_space,
-    lookupFunct  = #lookupFunct ML_Env.name_space,
+   {lookupVal    = #lookupVal ML_Env.local_name_space,
+    lookupType   = #lookupType ML_Env.local_name_space,
+    lookupFix    = #lookupFix ML_Env.local_name_space,
+    lookupStruct = #lookupStruct ML_Env.local_name_space,
+    lookupSig    = #lookupSig ML_Env.local_name_space,
+    lookupFunct  = #lookupFunct ML_Env.local_name_space,
     enterVal     = notify_val,
     enterType    = abort,
     enterFix     = abort,
     enterStruct  = abort,
     enterSig     = abort,
     enterFunct   = abort,
-    allVal       = #allVal ML_Env.name_space,
-    allType      = #allType ML_Env.name_space,
-    allFix       = #allFix ML_Env.name_space,
-    allStruct    = #allStruct ML_Env.name_space,
-    allSig       = #allSig ML_Env.name_space,
-    allFunct     = #allFunct ML_Env.name_space},
+    allVal       = #allVal ML_Env.local_name_space,
+    allType      = #allType ML_Env.local_name_space,
+    allFix       = #allFix ML_Env.local_name_space,
+    allStruct    = #allStruct ML_Env.local_name_space,
+    allSig       = #allSig ML_Env.local_name_space,
+    allFunct     = #allFunct ML_Env.local_name_space},
   str_of_pos = #str_of_pos ML_Env.local_context,
   print = #print ML_Env.local_context,
   error = #error ML_Env.local_context};
diff -r c00646996701 -r 874bdedb2313 src/Tools/SML/Examples.thy
--- a/src/Tools/SML/Examples.thy	Thu Apr 17 14:52:23 2014 +0200
+++ b/src/Tools/SML/Examples.thy	Sat Apr 19 17:23:05 2014 +0200
@@ -23,7 +23,6 @@
 
 SML_file "factorial.sml"
 
-
 text {*
   The subsequent example illustrates the use of multiple 'SML_file'
   commands to build larger Standard ML projects.  The toplevel SML
@@ -34,4 +33,20 @@
 SML_file "Example.sig"
 SML_file "Example.sml"
 
+
+text {*
+  Isabelle/ML and SML share a common run-time system, but the static
+  environments are separate.  It is possible to exchange toplevel bindings
+  via separate commands like this.
+*}
+
+SML_export {* val f = factorial *}  -- {* re-use factorial from SML environment *}
+ML {* f 42 *}
+
+SML_import {* val println = Output.writeln *}
+  -- {* re-use Isabelle/ML channel for SML *}
+
+SML_import {* val par_map = Par_List.map *}
+  -- {* re-use Isabelle/ML parallel list combinator for SML *}
+
 end