# HG changeset patch
# User wenzelm
# Date 1395774773 -3600
# Node ID fc4cf41d350483884e37360213d75344c5504c9c
# Parent  def3bbe6f2a53cf7c6088d5d1fc3641c28abed2f# Parent  20cf88cd3188cf0772c827d8ee4d1c1ff15d739d
merged

diff -r def3bbe6f2a5 -r fc4cf41d3504 Admin/components/components.sha1
--- a/Admin/components/components.sha1	Tue Mar 25 14:20:58 2014 +0100
+++ b/Admin/components/components.sha1	Tue Mar 25 20:12:53 2014 +0100
@@ -60,6 +60,7 @@
 f7dc7a4e1aea46408fd6e44b8cfacb33af61afbc  scala-2.10.1.tar.gz
 207e4916336335386589c918c5e3f3dcc14698f2  scala-2.10.2.tar.gz
 21c8ee274ffa471ab54d4196ecd827bf3d43e591  scala-2.10.3.tar.gz
+d4688ddaf83037ca43b5bf271325fc53ae70e3aa  scala-2.10.4.tar.gz
 b447017e81600cc5e30dd61b5d4962f6da01aa80  scala-2.8.1.final.tar.gz
 5659440f6b86db29f0c9c0de7249b7e24a647126  scala-2.9.2.tar.gz
 43b5afbcad575ab6817d2289756ca22fd2ef43a9  spass-3.8ds.tar.gz
diff -r def3bbe6f2a5 -r fc4cf41d3504 Admin/components/main
--- a/Admin/components/main	Tue Mar 25 14:20:58 2014 +0100
+++ b/Admin/components/main	Tue Mar 25 20:12:53 2014 +0100
@@ -8,7 +8,7 @@
 jfreechart-1.0.14-1
 kodkodi-1.5.2
 polyml-5.5.1-1
-scala-2.10.3
+scala-2.10.4
 spass-3.8ds
 z3-3.2-1
 z3-4.3.0
diff -r def3bbe6f2a5 -r fc4cf41d3504 NEWS
--- a/NEWS	Tue Mar 25 14:20:58 2014 +0100
+++ b/NEWS	Tue Mar 25 20:12:53 2014 +0100
@@ -34,9 +34,11 @@
 exception.  Potential INCOMPATIBILITY for non-conformant tactical
 proof tools.
 
-* Discontinued old Toplevel.debug in favour of system option
-"exception_trace", which may be also declared within the context via
-"declare [[exception_trace = true]]".  Minor INCOMPATIBILITY.
+* 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.
 
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
@@ -539,6 +541,18 @@
 
 *** ML ***
 
+* Discontinued old Toplevel.debug in favour of system option
+"ML_exception_trace", which may be also declared within the context via
+"declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
+
+* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
+INCOMPATIBILITY.
+
+* Configuration option "ML_print_depth" controls the pretty-printing
+depth of the ML compiler within the context.  The old print_depth in
+ML is still available as put_default_print_depth, but rarely used.
+Minor INCOMPATIBILITY.
+
 * Proper context discipline for read_instantiate and instantiate_tac:
 variables that are meant to become schematic need to be given as
 fixed, and are generalized by the explicit context of local variables.
diff -r def3bbe6f2a5 -r fc4cf41d3504 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Tue Mar 25 14:20:58 2014 +0100
+++ b/etc/isar-keywords-ZF.el	Tue Mar 25 20:12:53 2014 +0100
@@ -20,6 +20,7 @@
     "ProofGeneral\\.process_pgip"
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
+    "SML_file"
     "abbreviation"
     "also"
     "apply"
@@ -344,6 +345,7 @@
 (defconst isar-keywords-theory-decl
   '("ML"
     "ML_file"
+    "SML_file"
     "abbreviation"
     "attribute_setup"
     "axiomatization"
diff -r def3bbe6f2a5 -r fc4cf41d3504 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Mar 25 14:20:58 2014 +0100
+++ b/etc/isar-keywords.el	Tue Mar 25 20:12:53 2014 +0100
@@ -20,6 +20,7 @@
     "ProofGeneral\\.process_pgip"
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
+    "SML_file"
     "abbreviation"
     "adhoc_overloading"
     "also"
@@ -482,6 +483,7 @@
 (defconst isar-keywords-theory-decl
   '("ML"
     "ML_file"
+    "SML_file"
     "abbreviation"
     "adhoc_overloading"
     "atom_decl"
diff -r def3bbe6f2a5 -r fc4cf41d3504 etc/options
--- a/etc/options	Tue Mar 25 14:20:58 2014 +0100
+++ b/etc/options	Tue Mar 25 20:12:53 2014 +0100
@@ -97,8 +97,11 @@
 option process_output_limit : int = 100
   -- "build process output limit in million characters (0 = unlimited)"
 
-public option exception_trace : bool = false
-  -- "exception trace for toplevel command execution"
+
+section "ML System"
+
+public option ML_exception_trace : bool = false
+  -- "ML exception trace for toplevel command execution"
 
 
 section "Editor Reactivity"
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Doc/IsarRef/Inner_Syntax.thy
--- a/src/Doc/IsarRef/Inner_Syntax.thy	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -320,10 +320,11 @@
 text {*
   \begin{mldecls}
     @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
-    @{index_ML print_depth: "int -> unit"} \\
   \end{mldecls}
 
-  These ML functions set limits for pretty printed text.
+  \begin{tabular}{rcll}
+    @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\ %FIXME move?
+  \end{tabular}
 
   \begin{description}
 
@@ -334,9 +335,9 @@
   engine of Isabelle/ML altogether and do it within the front end via
   Isabelle/Scala.
 
-  \item @{ML print_depth}~@{text n} limits the printing depth of the
+  \item @{attribute ML_print_depth} limits the printing depth of the
   ML toplevel pretty printer; the precise effect depends on the ML
-  compiler and run-time system.  Typically @{text n} should be less
+  compiler and run-time system.  Typically the limit should be less
   than 10.  Bigger values such as 100--1000 are useful for debugging.
 
   \end{description}
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -1000,6 +1000,7 @@
 
 text {*
   \begin{matharray}{rcl}
+    @{command_def "SML_file"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\
@@ -1011,7 +1012,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command ML_file} @{syntax name}
+    (@@{command SML_file} | @@{command ML_file}) @{syntax name}
     ;
     (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
       @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
@@ -1021,6 +1022,14 @@
 
   \begin{description}
 
+  \item @{command "SML_file"}~@{text "name"} reads and evaluates the
+  given Standard ML file.  Top-level SML bindings are stored within
+  the theory context; the initial environment is restricted to the
+  Standard ML implementation of Poly/ML, without the many add-ons of
+  Isabelle/ML.  Multiple @{command "SML_file"} commands may be used to
+  build larger Standard ML projects, independently of the regular
+  Isabelle/ML environment.
+
   \item @{command "ML_file"}~@{text "name"} reads and evaluates the
   given ML file.  The current theory context is passed down to the ML
   toplevel and may be modified, using @{ML "Context.>>"} or derived ML
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -78,7 +78,7 @@
   | _ => error ("Single ML name expected in input: " ^ quote txt));
 
 fun prep_ml source =
-  (#1 (Symbol_Pos.source_content source), ML_Lex.read_source source);
+  (#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source);
 
 fun index_ml name kind ml = Thy_Output.antiquotation name
   (Scan.lift (Args.name_source_position -- Scan.option (Args.colon |-- Args.name_source_position)))
@@ -99,7 +99,9 @@
         else txt1 ^ " : " ^ txt2;
       val txt' = if kind = "" then txt else kind ^ " " ^ txt;
 
-      val _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2));
+      val _ =
+        ML_Context.eval_in (SOME ctxt) {SML = false, verbose = false} (#pos source1)
+          (ml (toks1, toks2));
       val kind' = if kind = "" then "ML" else "ML " ^ kind;
     in
       "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/Metis.thy
--- a/src/HOL/Metis.thy	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/Metis.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -10,7 +10,9 @@
 imports ATP
 begin
 
+declare [[ML_print_depth = 0]]
 ML_file "~~/src/Tools/Metis/metis.ML"
+declare [[ML_print_depth = 10]]
 
 subsection {* Literal selection and lambda-lifting helpers *}
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/TPTP/TPTP_Parser/make_mlyacclib
--- a/src/HOL/TPTP/TPTP_Parser/make_mlyacclib	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/make_mlyacclib	Tue Mar 25 20:12:53 2014 +0100
@@ -20,8 +20,6 @@
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (******************************************************************)
 
-print_depth 0;
-
 (*
   This file is generated from the contents of ML-Yacc's lib directory.
   ML-Yacc's COPYRIGHT-file contents follow:
@@ -48,7 +46,6 @@
 
   cat <<EOF
 ;
-print_depth 10;
 EOF
 
 ) > ml_yacc_lib.ML
\ No newline at end of file
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML
--- a/src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -5,8 +5,6 @@
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (******************************************************************)
 
-print_depth 0;
-
 (*
   This file is generated from the contents of ML-Yacc's lib directory.
   ML-Yacc's COPYRIGHT-file contents follow:
@@ -1061,4 +1059,3 @@
  end;
 
 ;
-print_depth 10;
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -285,7 +285,7 @@
 
 type tptp_problem = tptp_line list
 
-fun debug f x = if Options.default_bool @{option exception_trace} then (f x; ()) else ()
+fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
 
 fun nameof_tff_atom_type (Atom_type str) = str
   | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -42,8 +42,8 @@
 ML {*
   if test_all @{context} then ()
   else
-    (Options.default_put_bool @{option exception_trace} true;
-     PolyML.print_depth 200;
+    (Options.default_put_bool @{option ML_exception_trace} true;
+     put_default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
      PolyML.Compiler.maxInlineSize := 0)
 *}
 
@@ -186,8 +186,9 @@
      prob_names;
 *}
 
+declare [[ML_print_depth = 2000]]
+
 ML {*
-print_depth 2000;
 the_tactics
 |> map (filter (fn (_, _, x) => is_none x)
         #> map (fn (x, SOME y, _) => (x, cterm_of @{theory} y)))
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -11,9 +11,8 @@
 imports TPTP_Test TPTP_Proof_Reconstruction
 begin
 
-declare [[exception_trace]]
+declare [[ML_exception_trace, ML_print_depth = 200]]
 ML {*
-print_depth 200;
 PolyML.Compiler.maxInlineSize := 0;
 (* FIXME doesn't work with Isabelle?
    PolyML.Compiler.debug := true *)
@@ -2025,8 +2024,7 @@
 
 (*SYN044^4*)
 (*
-ML {*
-print_depth 1400;
+declare [[ML_print_depth = 1400]]
 (* the_tactics *)
 *}
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/Tools/numeral_simprocs.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -738,144 +738,3 @@
 
 end;
 
-(*examples:
-print_depth 22;
-set timing;
-set simp_trace;
-fun test s = (Goal s, by (Simp_tac 1));
-
-test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)";
-
-test "2*u = (u::int)";
-test "(i + j + 12 + (k::int)) - 15 = y";
-test "(i + j + 12 + (k::int)) - 5 = y";
-
-test "y - b < (b::int)";
-test "y - (3*b + c) < (b::int) - 2*c";
-
-test "(2*x - (u*v) + y) - v*3*u = (w::int)";
-test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)";
-test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)";
-test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)";
-
-test "(i + j + 12 + (k::int)) = u + 15 + y";
-test "(i + j*2 + 12 + (k::int)) = j + 5 + y";
-
-test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)";
-
-test "a + -(b+c) + b = (d::int)";
-test "a + -(b+c) - b = (d::int)";
-
-(*negative numerals*)
-test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz";
-test "(i + j + -3 + (k::int)) < u + 5 + y";
-test "(i + j + 3 + (k::int)) < u + -6 + y";
-test "(i + j + -12 + (k::int)) - 15 = y";
-test "(i + j + 12 + (k::int)) - -15 = y";
-test "(i + j + -12 + (k::int)) - -15 = y";
-*)
-
-(*examples:
-print_depth 22;
-set timing;
-set simp_trace;
-fun test s = (Goal s; by (Simp_tac 1));
-
-test "9*x = 12 * (y::int)";
-test "(9*x) div (12 * (y::int)) = z";
-test "9*x < 12 * (y::int)";
-test "9*x <= 12 * (y::int)";
-
-test "-99*x = 132 * (y::int)";
-test "(-99*x) div (132 * (y::int)) = z";
-test "-99*x < 132 * (y::int)";
-test "-99*x <= 132 * (y::int)";
-
-test "999*x = -396 * (y::int)";
-test "(999*x) div (-396 * (y::int)) = z";
-test "999*x < -396 * (y::int)";
-test "999*x <= -396 * (y::int)";
-
-test "-99*x = -81 * (y::int)";
-test "(-99*x) div (-81 * (y::int)) = z";
-test "-99*x <= -81 * (y::int)";
-test "-99*x < -81 * (y::int)";
-
-test "-2 * x = -1 * (y::int)";
-test "-2 * x = -(y::int)";
-test "(-2 * x) div (-1 * (y::int)) = z";
-test "-2 * x < -(y::int)";
-test "-2 * x <= -1 * (y::int)";
-test "-x < -23 * (y::int)";
-test "-x <= -23 * (y::int)";
-*)
-
-(*And the same examples for fields such as rat or real:
-test "0 <= (y::rat) * -2";
-test "9*x = 12 * (y::rat)";
-test "(9*x) / (12 * (y::rat)) = z";
-test "9*x < 12 * (y::rat)";
-test "9*x <= 12 * (y::rat)";
-
-test "-99*x = 132 * (y::rat)";
-test "(-99*x) / (132 * (y::rat)) = z";
-test "-99*x < 132 * (y::rat)";
-test "-99*x <= 132 * (y::rat)";
-
-test "999*x = -396 * (y::rat)";
-test "(999*x) / (-396 * (y::rat)) = z";
-test "999*x < -396 * (y::rat)";
-test "999*x <= -396 * (y::rat)";
-
-test  "(- ((2::rat) * x) <= 2 * y)";
-test "-99*x = -81 * (y::rat)";
-test "(-99*x) / (-81 * (y::rat)) = z";
-test "-99*x <= -81 * (y::rat)";
-test "-99*x < -81 * (y::rat)";
-
-test "-2 * x = -1 * (y::rat)";
-test "-2 * x = -(y::rat)";
-test "(-2 * x) / (-1 * (y::rat)) = z";
-test "-2 * x < -(y::rat)";
-test "-2 * x <= -1 * (y::rat)";
-test "-x < -23 * (y::rat)";
-test "-x <= -23 * (y::rat)";
-*)
-
-(*examples:
-print_depth 22;
-set timing;
-set simp_trace;
-fun test s = (Goal s; by (Asm_simp_tac 1));
-
-test "x*k = k*(y::int)";
-test "k = k*(y::int)";
-test "a*(b*c) = (b::int)";
-test "a*(b*c) = d*(b::int)*(x*a)";
-
-test "(x*k) div (k*(y::int)) = (uu::int)";
-test "(k) div (k*(y::int)) = (uu::int)";
-test "(a*(b*c)) div ((b::int)) = (uu::int)";
-test "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)";
-*)
-
-(*And the same examples for fields such as rat or real:
-print_depth 22;
-set timing;
-set simp_trace;
-fun test s = (Goal s; by (Asm_simp_tac 1));
-
-test "x*k = k*(y::rat)";
-test "k = k*(y::rat)";
-test "a*(b*c) = (b::rat)";
-test "a*(b*c) = d*(b::rat)*(x*a)";
-
-
-test "(x*k) / (k*(y::rat)) = (uu::rat)";
-test "(k) / (k*(y::rat)) = (uu::rat)";
-test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
-test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
-
-(*FIXME: what do we do about this?*)
-test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
-*)
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/ex/Cartouche_Examples.thy
--- a/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -118,9 +118,9 @@
       let
         val toks =
           ML_Lex.read Position.none "fn _ => (" @
-          ML_Lex.read_source source @
+          ML_Lex.read_source false source @
           ML_Lex.read Position.none ");";
-        val _ = ML_Context.eval_in (SOME context) false (#pos source) toks;
+        val _ = ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) toks;
       in "" end);
 *}
 
@@ -189,7 +189,7 @@
       val ctxt' = ctxt |> Context.proof_map
         (ML_Context.expression (#pos source)
           "fun tactic (ctxt : Proof.context) : tactic"
-          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source source));
+          "Context.map_proof (ML_Tactic.set tactic)" (ML_Lex.read_source false source));
     in Data.get ctxt' ctxt end;
 end;
 *}
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/HOL/ex/ML.thy
--- a/src/HOL/ex/ML.thy	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/HOL/ex/ML.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -121,7 +121,7 @@
 term "factorial 4"  -- "symbolic term"
 value "factorial 4"  -- "evaluation via ML code generation in the background"
 
-declare [[ML_trace]]
+declare [[ML_source_trace]]
 ML {* @{term "factorial 4"} *}  -- "symbolic term in ML"
 ML {* @{code "factorial"} *}  -- "ML code from function specification"
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/General/completion.scala	Tue Mar 25 20:12:53 2014 +0100
@@ -193,6 +193,7 @@
     val inner = Language_Context(Markup.Language.UNKNOWN, true, false)
     val ML_outer = Language_Context(Markup.Language.ML, false, true)
     val ML_inner = Language_Context(Markup.Language.ML, true, false)
+    val SML_outer = Language_Context(Markup.Language.SML, false, false)
   }
 
   sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean)
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -181,7 +181,7 @@
     "val (name, scan, comment): binding * attribute context_parser * string"
     "Context.map_theory (Attrib.setup name scan comment)"
     (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-      ML_Lex.read_source source @
+      ML_Lex.read_source false source @
       ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
 
 
@@ -457,7 +457,8 @@
   register_config Name_Space.names_long_raw #>
   register_config Name_Space.names_short_raw #>
   register_config Name_Space.names_unique_raw #>
-  register_config ML_Context.trace_raw #>
+  register_config ML_Context.source_trace_raw #>
+  register_config ML_Compiler.print_depth_raw #>
   register_config Runtime.exception_trace_raw #>
   register_config Proof_Context.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -67,12 +67,12 @@
 (* generic setup *)
 
 fun global_setup source =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source) "val setup: theory -> theory" "Context.map_theory setup"
   |> Context.theory_map;
 
 fun local_setup source =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source) "val setup: local_theory -> local_theory" "Context.map_proof setup"
   |> Context.proof_map;
 
@@ -80,35 +80,35 @@
 (* translation functions *)
 
 fun parse_ast_translation source =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source)
     "val parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
     "Context.map_theory (Sign.parse_ast_translation parse_ast_translation)"
   |> Context.theory_map;
 
 fun parse_translation source =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source)
     "val parse_translation: (string * (Proof.context -> term list -> term)) list"
     "Context.map_theory (Sign.parse_translation parse_translation)"
   |> Context.theory_map;
 
 fun print_translation source =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source)
     "val print_translation: (string * (Proof.context -> term list -> term)) list"
     "Context.map_theory (Sign.print_translation print_translation)"
   |> Context.theory_map;
 
 fun typed_print_translation source =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source)
     "val typed_print_translation: (string * (Proof.context -> typ -> term list -> term)) list"
     "Context.map_theory (Sign.typed_print_translation typed_print_translation)"
   |> Context.theory_map;
 
 fun print_ast_translation source =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source)
     "val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list"
     "Context.map_theory (Sign.print_ast_translation print_ast_translation)"
@@ -135,7 +135,7 @@
 
 fun oracle (name, pos) source =
   let
-    val body = ML_Lex.read_source source;
+    val body = ML_Lex.read_source false source;
     val ants =
       ML_Lex.read Position.none
        ("local\n\
@@ -145,7 +145,8 @@
         \  val " ^ name ^
         " = snd (Context.>>> (Context.map_theory_result (Thm.add_oracle (binding, body))));\n\
         \end;\n");
-  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval false (#pos source) ants)) end;
+    val flags = {SML = false, verbose = false};
+  in Context.theory_map (ML_Context.exec (fn () => ML_Context.eval flags (#pos source) ants)) end;
 
 
 (* old-style defs *)
@@ -161,7 +162,7 @@
 (* declarations *)
 
 fun declaration {syntax, pervasive} source =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source)
     "val declaration: Morphism.declaration"
     ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
@@ -172,7 +173,7 @@
 (* simprocs *)
 
 fun simproc_setup name lhss source identifier =
-  ML_Lex.read_source source
+  ML_Lex.read_source false source
   |> ML_Context.expression (#pos source)
     "val proc: Morphism.morphism -> Proof.context -> cterm -> thm option"
     ("Context.map_proof (Simplifier.def_simproc_cmd {name = " ^ ML_Syntax.make_binding name ^ ", \
@@ -238,7 +239,7 @@
   let val opt_ctxt =
     try Toplevel.generic_theory_of state
     |> Option.map (Context.proof_of #> Diag_State.put state)
-  in ML_Context.eval_source_in opt_ctxt verbose source end);
+  in ML_Context.eval_source_in opt_ctxt {SML = false, verbose = verbose} source end);
 
 val diag_state = Diag_State.get;
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -268,17 +268,28 @@
 (* use ML text *)
 
 val _ =
+  Outer_Syntax.command @{command_spec "SML_file"} "read and evaluate Standard ML file"
+    (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
+        let
+          val ([{lines, pos, ...}], thy') = files thy;
+          val source = {delimited = true, text = cat_lines lines, pos = pos};
+        in
+          thy' |> Context.theory_map
+            (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source))
+        end)));
+
+val _ =
   Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
     (Parse.ML_source >> (fn source =>
       Toplevel.generic_theory
-        (ML_Context.exec (fn () => ML_Context.eval_source true source) #>
+        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #>
           Local_Theory.propagate_ml_env)));
 
 val _ =
   Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
     (Parse.ML_source >> (fn source =>
       Toplevel.proof (Proof.map_context (Context.proof_map
-        (ML_Context.exec (fn () => ML_Context.eval_source true source))) #>
+        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #>
           Proof.propagate_ml_env)));
 
 val _ =
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Isar/method.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -269,7 +269,7 @@
     val ctxt' = ctxt |> Context.proof_map
       (ML_Context.expression (#pos source)
         "fun tactic (facts: thm list) : tactic"
-        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source source));
+        "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read_source false source));
   in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
 
 fun tactic source ctxt = METHOD (ml_tactic source ctxt);
@@ -368,7 +368,7 @@
     "val (name, scan, comment): binding * (Proof.context -> Proof.method) context_parser * string"
     "Context.map_theory (Method.setup name scan comment)"
     (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-      ML_Lex.read_source source @
+      ML_Lex.read_source false source @
       ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));
 
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Isar/runtime.ML
--- a/src/Pure/Isar/runtime.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Isar/runtime.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -136,7 +136,7 @@
 
 (** controlled execution **)
 
-val exception_trace_raw = Config.declare_option "exception_trace";
+val exception_trace_raw = Config.declare_option "ML_exception_trace";
 val exception_trace = Config.bool exception_trace_raw;
 
 fun exception_trace_enabled NONE =
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML-Systems/ml_name_space.ML
--- a/src/Pure/ML-Systems/ml_name_space.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML-Systems/ml_name_space.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -54,4 +54,11 @@
   allSig = fn _ => [],
   allFunct = fn _ => []};
 
+val initial_val : (string * valueVal) list = [];
+val initial_type : (string * typeVal) list = [];
+val initial_fixity : (string * fixityVal) list = [];
+val initial_structure : (string * structureVal) list = [];
+val initial_signature : (string * signatureVal) list = [];
+val initial_functor : (string * functorVal) list = [];
+
 end;
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -4,6 +4,24 @@
 Compatibility wrapper for Poly/ML.
 *)
 
+(* ML name space *)
+
+structure ML_Name_Space =
+struct
+  open PolyML.NameSpace;
+  type T = PolyML.NameSpace.nameSpace;
+  val global = PolyML.globalNameSpace;
+  val initial_val =
+    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
+      (#allVal global ());
+  val initial_type = #allType global ();
+  val initial_fixity = #allFix global ();
+  val initial_structure = #allStruct global ();
+  val initial_signature = #allSig global ();
+  val initial_functor = #allFunct global ();
+end;
+
+
 (* ML system operations *)
 
 use "ML-Systems/ml_system.ML";
@@ -94,20 +112,12 @@
 
 (* ML compiler *)
 
-structure ML_Name_Space =
-struct
-  open PolyML.NameSpace;
-  type T = PolyML.NameSpace.nameSpace;
-  val global = PolyML.globalNameSpace;
-end;
-
 use "ML-Systems/use_context.ML";
 use "ML-Systems/compiler_polyml.ML";
 
 PolyML.Compiler.reportUnreferencedIds := true;
 PolyML.Compiler.printInAlphabeticalOrder := false;
 PolyML.Compiler.maxInlineSize := 80;
-(*PolyML.Compiler.reportExhaustiveHandlers := true;*)
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
@@ -119,8 +129,9 @@
 local
   val depth = Unsynchronized.ref 10;
 in
-  fun get_print_depth () = ! depth;
-  fun print_depth n = (depth := n; PolyML.print_depth n);
+  fun get_default_print_depth () = ! depth;
+  fun put_default_print_depth n = (depth := n; PolyML.print_depth n);
+  val _ = put_default_print_depth 10;
 end;
 
 val error_depth = PolyML.error_depth;
@@ -164,5 +175,5 @@
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
 val ml_make_string =
-  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
+  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))";
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -56,11 +56,12 @@
 local
   val depth = ref (10: int);
 in
-  fun get_print_depth () = ! depth;
-  fun print_depth n =
+  fun get_default_print_depth () = ! depth;
+  fun put_default_print_depth n =
    (depth := n;
     Control.Print.printDepth := dest_int n div 2;
     Control.Print.printLength := dest_int n);
+  val _ = put_default_print_depth 10;
 end;
 
 val ml_make_string = "(fn _ => \"?\")";
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML/exn_trace_polyml-5.5.1.ML
--- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -12,3 +12,5 @@
         val _ = tracing (cat_lines (title :: trace));
       in reraise exn end);
 
+PolyML.Compiler.reportExhaustiveHandlers := true;
+
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -11,12 +11,18 @@
   val exn_message: exn -> string
   val exn_error_message: exn -> unit
   val exn_trace: (unit -> 'a) -> 'a
-  val eval: bool -> Position.T -> ML_Lex.token list -> unit
+  val print_depth_raw: Config.raw
+  val print_depth: int Config.T
+  val get_print_depth: unit -> int
+  type flags = {SML: bool, verbose: bool}
+  val eval: flags -> Position.T -> ML_Lex.token list -> unit
 end
 
 structure ML_Compiler: ML_COMPILER =
 struct
 
+(* exceptions *)
+
 val exn_info =
  {exn_position = fn _: exn => Position.none,
   pretty_exn = Pretty.str o General.exnMessage};
@@ -28,8 +34,26 @@
 val exn_error_message = Output.error_message o exn_message;
 fun exn_trace e = print_exception_trace exn_message e;
 
-fun eval verbose pos toks =
+
+(* print depth *)
+
+val print_depth_raw =
+  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
+val print_depth = Config.int print_depth_raw;
+
+fun get_print_depth () =
+  (case Context.thread_data () of
+    NONE => get_default_print_depth ()
+  | SOME context => Config.get_generic context print_depth);
+
+
+(* eval *)
+
+type flags = {SML: bool, verbose: bool};
+
+fun eval {SML, verbose} pos toks =
   let
+    val _ = if SML then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
     val line = the_default 1 (Position.line_of pos);
     val file = the_default "ML" (Position.file_of pos);
     val text = ML_Lex.flatten toks;
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -7,6 +7,9 @@
 structure ML_Compiler: ML_COMPILER =
 struct
 
+open ML_Compiler;
+
+
 (* source locations *)
 
 fun position_of (loc: PolyML.location) =
@@ -74,10 +77,10 @@
 
 (* eval ML source tokens *)
 
-fun eval verbose pos toks =
+fun eval {SML, verbose} pos toks =
   let
     val _ = Secure.secure_mltext ();
-    val space = ML_Env.name_space;
+    val space = if SML then ML_Env.SML_name_space else ML_Env.name_space;
     val opt_context = Context.thread_data ();
 
 
@@ -182,6 +185,7 @@
       PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
       PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
       PolyML.Compiler.CPFileName location_props,
+      PolyML.Compiler.CPPrintDepth get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false];
     val _ =
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -17,16 +17,16 @@
   val add_antiquotation: binding -> (Args.src -> Proof.context -> decl * Proof.context) ->
     theory -> theory
   val print_antiquotations: Proof.context -> unit
-  val trace_raw: Config.raw
-  val trace: bool Config.T
+  val source_trace_raw: Config.raw
+  val source_trace: bool Config.T
   val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
-  val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
-  val eval_file: bool -> Path.T -> unit
-  val eval_source: bool -> Symbol_Pos.source -> unit
-  val eval_in: Proof.context option -> bool -> Position.T ->
+  val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
+  val eval_file: ML_Compiler.flags -> Path.T -> unit
+  val eval_source: ML_Compiler.flags -> Symbol_Pos.source -> unit
+  val eval_in: Proof.context option -> ML_Compiler.flags -> Position.T ->
     ML_Lex.token Antiquote.antiquote list -> unit
-  val eval_source_in: Proof.context option -> bool -> Symbol_Pos.source -> unit
+  val eval_source_in: Proof.context option -> ML_Compiler.flags -> Symbol_Pos.source -> unit
   val expression: Position.T -> string -> string -> ML_Lex.token Antiquote.antiquote list ->
     Context.generic -> Context.generic
 end
@@ -137,17 +137,19 @@
         in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
   in ((ml_env @ end_env, ml_body), opt_ctxt') end;
 
-val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);
-val trace = Config.bool trace_raw;
+val source_trace_raw = Config.declare "ML_source_trace" (fn _ => Config.Bool false);
+val source_trace = Config.bool source_trace_raw;
 
-fun eval verbose pos ants =
+fun eval flags pos ants =
   let
+    val non_verbose = {SML = #SML flags, verbose = false};
+
     (*prepare source text*)
     val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
     val _ =
       (case Option.map Context.proof_of env_ctxt of
         SOME ctxt =>
-          if Config.get ctxt trace then
+          if Config.get ctxt source_trace then
             Context_Position.if_visible ctxt
               tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
           else ()
@@ -157,11 +159,11 @@
     val _ =
       Context.setmp_thread_data
         (Option.map (Context.mapping I (Context_Position.set_visible false)) env_ctxt)
-        (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) ()
+        (fn () => (ML_Compiler.eval non_verbose Position.none env; Context.thread_data ())) ()
       |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
 
-    val _ = ML_Compiler.eval verbose pos body;
-    val _ = ML_Compiler.eval false Position.none reset_env;
+    val _ = ML_Compiler.eval flags pos body;
+    val _ = ML_Compiler.eval non_verbose Position.none reset_env;
   in () end;
 
 end;
@@ -169,29 +171,29 @@
 
 (* derived versions *)
 
-fun eval_file verbose path =
+fun eval_file flags path =
   let val pos = Path.position path
-  in eval verbose pos (ML_Lex.read pos (File.read path)) end;
+  in eval flags pos (ML_Lex.read pos (File.read path)) end;
 
-fun eval_source verbose source =
-  eval verbose (#pos source) (ML_Lex.read_source source);
+fun eval_source flags source =
+  eval flags (#pos source) (ML_Lex.read_source (#SML flags) source);
 
-fun eval_in ctxt verbose pos ants =
+fun eval_in ctxt flags pos ants =
   Context.setmp_thread_data (Option.map Context.Proof ctxt)
-    (fn () => eval verbose pos ants) ();
+    (fn () => eval flags pos ants) ();
 
-fun eval_source_in ctxt verbose source =
+fun eval_source_in ctxt flags source =
   Context.setmp_thread_data (Option.map Context.Proof ctxt)
-    (fn () => eval_source verbose source) ();
+    (fn () => eval_source flags source) ();
 
 fun expression pos bind body ants =
-  exec (fn () => eval false pos
+  exec (fn () => eval {SML = false, verbose = false} pos
     (ML_Lex.read Position.none ("Context.set_thread_data (SOME (let " ^ bind ^ " = ") @ ants @
       ML_Lex.read Position.none (" in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
 
 end;
 
 fun use s =
-  ML_Context.eval_file true (Path.explode s)
+  ML_Context.eval_file {SML = false, verbose = true} (Path.explode s)
     handle ERROR msg => (writeln msg; error "ML error");
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML/ml_env.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -1,12 +1,14 @@
 (*  Title:      Pure/ML/ml_env.ML
     Author:     Makarius
 
-Local environment of ML results.
+Toplevel environment for Standard ML and Isabelle/ML within the
+implicit context.
 *)
 
 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 local_context: use_context
   val check_functor: string -> unit
@@ -17,56 +19,112 @@
 
 (* context data *)
 
+type tables =
+  ML_Name_Space.valueVal Symtab.table *
+  ML_Name_Space.typeVal Symtab.table *
+  ML_Name_Space.fixityVal Symtab.table *
+  ML_Name_Space.structureVal Symtab.table *
+  ML_Name_Space.signatureVal Symtab.table *
+  ML_Name_Space.functorVal Symtab.table;
+
+fun merge_tables
+  ((val1, type1, fixity1, structure1, signature1, functor1),
+   (val2, type2, fixity2, structure2, signature2, functor2)) : tables =
+  (Symtab.merge (K true) (val1, val2),
+   Symtab.merge (K true) (type1, type2),
+   Symtab.merge (K true) (fixity1, fixity2),
+   Symtab.merge (K true) (structure1, structure2),
+   Symtab.merge (K true) (signature1, signature2),
+   Symtab.merge (K true) (functor1, functor2));
+
+type data = {bootstrap: bool, tables: tables, sml_tables: tables};
+
+fun make_data (bootstrap, tables, sml_tables) : data =
+  {bootstrap = bootstrap, tables = tables, sml_tables = sml_tables};
+
 structure Env = Generic_Data
 (
-  type T =
-    bool * (*global bootstrap environment*)
-     (ML_Name_Space.valueVal Symtab.table *
-      ML_Name_Space.typeVal Symtab.table *
-      ML_Name_Space.fixityVal Symtab.table *
-      ML_Name_Space.structureVal Symtab.table *
-      ML_Name_Space.signatureVal Symtab.table *
-      ML_Name_Space.functorVal Symtab.table);
-  val empty : T =
-    (true, (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
-  fun extend (_, tabs) : T = (false, tabs);
-  fun merge
-   ((_, (val1, type1, fixity1, structure1, signature1, functor1)),
-    (_, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
-    (false,
-     (Symtab.merge (K true) (val1, val2),
-      Symtab.merge (K true) (type1, type2),
-      Symtab.merge (K true) (fixity1, fixity2),
-      Symtab.merge (K true) (structure1, structure2),
-      Symtab.merge (K true) (signature1, signature2),
-      Symtab.merge (K true) (functor1, functor2)));
+  type T = data
+  val empty =
+    make_data (true,
+      (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty),
+      (Symtab.make ML_Name_Space.initial_val,
+       Symtab.make ML_Name_Space.initial_type,
+       Symtab.make ML_Name_Space.initial_fixity,
+       Symtab.make ML_Name_Space.initial_structure,
+       Symtab.make ML_Name_Space.initial_signature,
+       Symtab.make ML_Name_Space.initial_functor));
+  fun extend (data : T) = make_data (false, #tables data, #sml_tables data);
+  fun merge (data : T * T) =
+    make_data (false,
+      merge_tables (pairself #tables data),
+      merge_tables (pairself #sml_tables data));
 );
 
 val inherit = Env.put o Env.get;
 
 
-(* results *)
+(* 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);
+
+    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 =
   let
     fun lookup sel1 sel2 name =
       Context.thread_data ()
-      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
+      |> (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 (#2 (Env.get context))))
+      |> (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
-        Context.>> (Env.map (fn (global, tabs) =>
+        Context.>> (Env.map (fn {bootstrap, tables, sml_tables} =>
           let
-            val _ = if global then sel2 ML_Name_Space.global entry else ();
-            val tabs' = ap1 (Symtab.update entry) tabs;
-          in (global, tabs') end))
+            val _ = if bootstrap then sel2 ML_Name_Space.global entry else ();
+            val tables' = ap1 (Symtab.update entry) tables;
+          in make_data (bootstrap, tables', sml_tables) end))
       else sel2 ML_Name_Space.global entry;
   in
    {lookupVal    = lookup #1 #lookupVal,
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -26,7 +26,7 @@
       Source.source) Source.source
   val tokenize: string -> token list
   val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
-  val read_source: Symbol_Pos.source -> token Antiquote.antiquote list
+  val read_source: bool -> Symbol_Pos.source -> token Antiquote.antiquote list
 end;
 
 structure ML_Lex: ML_LEX =
@@ -132,7 +132,7 @@
 
 local
 
-val token_kind_markup =
+fun token_kind_markup SML =
  fn Keyword   => (Markup.empty, "")
   | Ident     => (Markup.empty, "")
   | LongIdent => (Markup.empty, "")
@@ -141,18 +141,18 @@
   | Int       => (Markup.ML_numeral, "")
   | Real      => (Markup.ML_numeral, "")
   | Char      => (Markup.ML_char, "")
-  | String    => (Markup.ML_string, "")
+  | String    => (if SML then Markup.SML_string else Markup.ML_string, "")
   | Space     => (Markup.empty, "")
-  | Comment   => (Markup.ML_comment, "")
+  | Comment   => (if SML then Markup.SML_comment else Markup.ML_comment, "")
   | Error msg => (Markup.bad, msg)
   | EOF       => (Markup.empty, "");
 
 in
 
-fun report_of_token (tok as Token ((pos, _), (kind, x))) =
+fun report_of_token SML (tok as Token ((pos, _), (kind, x))) =
   let
     val (markup, txt) =
-      if not (is_keyword tok) then token_kind_markup kind
+      if not (is_keyword tok) then token_kind_markup SML kind
       else if is_delimiter tok then (Markup.ML_delimiter, "")
       else if member (op =) keywords2 x then (Markup.ML_keyword2, "")
       else if member (op =) keywords3 x then (Markup.ML_keyword3, "")
@@ -291,15 +291,7 @@
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> single)
   >> (single o token (Error msg));
 
-in
-
-fun source src =
-  Symbol_Pos.source (Position.line 1) src
-  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
-
-val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
-
-fun read pos text =
+fun gen_read SML pos text =
   let
     val syms = Symbol_Pos.explode (text, pos);
     val termination =
@@ -309,17 +301,32 @@
           val pos1 = List.last syms |-> Position.advance;
           val pos2 = Position.advance Symbol.space pos1;
         in [Antiquote.Text (Token (Position.range pos1 pos2, (Space, Symbol.space)))] end;
+
+    val scan = if SML then scan_ml >> Antiquote.Text else scan_antiq;
+    fun check (Antiquote.Text tok) = (check_content_of tok; if SML then () else warn tok)
+      | check _ = ();
     val input =
-      (Source.of_list syms
-        |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
-          (SOME (false, fn msg => recover msg >> map Antiquote.Text))
-        |> Source.exhaust
-        |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token))
-        |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
+      Source.of_list syms
+      |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan))
+        (SOME (false, fn msg => recover msg >> map Antiquote.Text))
+      |> Source.exhaust
+      |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token SML))
+      |> tap (List.app check);
   in input @ termination end;
 
-fun read_source {delimited, text, pos} =
-  (Position.report pos (Markup.language_ML delimited); read pos text);
+in
+
+fun source src =
+  Symbol_Pos.source (Position.line 1) src
+  |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
+
+val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
+
+val read = gen_read false;
+
+fun read_source SML {delimited, text, pos} =
+  (Position.report pos ((if SML then Markup.language_SML else Markup.language_ML) delimited);
+   gen_read SML pos text);
 
 end;
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala	Tue Mar 25 20:12:53 2014 +0100
@@ -239,13 +239,15 @@
 
     def token: Parser[Token] = delimited_token | other_token
 
-    def token_line(ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
+    def token_line(SML: Boolean, ctxt: Scan.Line_Context): Parser[(Token, Scan.Line_Context)] =
     {
       val other = (ml_char | other_token) ^^ (x => (x, Scan.Finished))
 
-      ml_string_line(ctxt) |
-        (ml_comment_line(ctxt) |
-          (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
+      if (SML) ml_string_line(ctxt) | (ml_comment_line(ctxt) | other)
+      else
+        ml_string_line(ctxt) |
+          (ml_comment_line(ctxt) |
+            (ml_antiq_start(ctxt) | (ml_antiq_stop(ctxt) | (ml_antiq_body(ctxt) | other))))
     }
   }
 
@@ -260,14 +262,14 @@
     }
   }
 
-  def tokenize_line(input: CharSequence, context: Scan.Line_Context)
+  def tokenize_line(SML: Boolean, input: CharSequence, context: Scan.Line_Context)
     : (List[Token], Scan.Line_Context) =
   {
     var in: Reader[Char] = new CharSequenceReader(input)
     val toks = new mutable.ListBuffer[Token]
     var ctxt = context
     while (!in.atEnd) {
-      Parsers.parse(Parsers.token_line(ctxt), in) match {
+      Parsers.parse(Parsers.token_line(SML, ctxt), in) match {
         case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
         case Parsers.NoSuccess(_, rest) =>
           error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -130,7 +130,7 @@
       else if not (ML_Syntax.is_identifier name) then
         error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
       else
-        ML_Compiler.eval true Position.none
+        ML_Compiler.eval {SML = false, verbose = true} Position.none
           (ML_Lex.tokenize ("val " ^ name ^ " = " ^ get ^ " ();"));
     val _ = Theory.setup (Stored_Thms.put []);
   in () end;
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -33,6 +33,7 @@
   val language_term: bool -> T
   val language_prop: bool -> T
   val language_ML: bool -> T
+  val language_SML: bool -> T
   val language_document: bool -> T
   val language_antiquotation: T
   val language_text: bool -> T
@@ -93,6 +94,8 @@
   val ML_charN: string val ML_char: T
   val ML_stringN: string val ML_string: T
   val ML_commentN: string val ML_comment: T
+  val SML_stringN: string val SML_string: T
+  val SML_commentN: string val SML_comment: T
   val ML_defN: string
   val ML_openN: string
   val ML_structureN: string
@@ -287,6 +290,7 @@
 val language_term = language' {name = "term", symbols = true, antiquotes = false};
 val language_prop = language' {name = "prop", symbols = true, antiquotes = false};
 val language_ML = language' {name = "ML", symbols = false, antiquotes = true};
+val language_SML = language' {name = "SML", symbols = false, antiquotes = false};
 val language_document = language' {name = "document", symbols = false, antiquotes = true};
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
@@ -398,6 +402,8 @@
 val (ML_charN, ML_char) = markup_elem "ML_char";
 val (ML_stringN, ML_string) = markup_elem "ML_string";
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
+val (SML_stringN, SML_string) = markup_elem "SML_string";
+val (SML_commentN, SML_comment) = markup_elem "SML_comment";
 
 val ML_defN = "ML_def";
 val ML_openN = "ML_open";
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Tue Mar 25 20:12:53 2014 +0100
@@ -101,6 +101,7 @@
   object Language
   {
     val ML = "ML"
+    val SML = "SML"
     val UNKNOWN = "unknown"
 
     def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] =
@@ -202,6 +203,8 @@
   val ML_CHAR = "ML_char"
   val ML_STRING = "ML_string"
   val ML_COMMENT = "ML_comment"
+  val SML_STRING = "SML_string"
+  val SML_COMMENT = "SML_comment"
 
   val ML_DEF = "ML_def"
   val ML_OPEN = "ML_open"
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Pure.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -14,7 +14,7 @@
     "infixr" "is" "keywords" "notes" "obtains" "open" "output"
     "overloaded" "pervasive" "shows" "structure" "unchecked" "where" "|"
   and "theory" :: thy_begin % "theory"
-  and "ML_file" :: thy_load % "ML"
+  and "SML_file" "ML_file" :: thy_load % "ML"
   and "header" :: diag
   and "chapter" :: thy_heading1
   and "section" :: thy_heading2
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -6,8 +6,6 @@
   val is_official = false;
 end;
 
-print_depth 10;
-
 
 (* library of general tools *)
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -639,7 +639,7 @@
 
 fun ml_text name ml = antiquotation name (Scan.lift Args.name_source_position)
   (fn {context, ...} => fn source =>
-   (ML_Context.eval_in (SOME context) false (#pos source) (ml source);
+   (ML_Context.eval_in (SOME context) {SML = false, verbose = false} (#pos source) (ml source);
     Symbol_Pos.source_content source
     |> #1
     |> (if Config.get context quotes then quote else I)
@@ -648,7 +648,7 @@
 
 fun ml_enclose bg en source =
   ML_Lex.read Position.none bg @
-  ML_Lex.read_source source @
+  ML_Lex.read_source false source @
   ML_Lex.read Position.none en;
 
 in
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Tools/doc.scala
--- a/src/Pure/Tools/doc.scala	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Tools/doc.scala	Tue Mar 25 20:12:53 2014 +0100
@@ -61,7 +61,8 @@
         "src/HOL/ex/Seq.thy",
         "src/HOL/ex/ML.thy",
         "src/HOL/Unix/Unix.thy",
-        "src/HOL/Isar_Examples/Drinker.thy")
+        "src/HOL/Isar_Examples/Drinker.thy",
+        "src/Tools/SML/Examples.thy")
     Section("Examples") :: names.map(name => text_file(name).get)
   }
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/Tools/proof_general_pure.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -76,8 +76,8 @@
 val _ =
   ProofGeneral.preference ProofGeneral.category_advanced_display
     NONE
-    (Markup.print_int o get_print_depth)
-    (print_depth o Markup.parse_int)
+    (Markup.print_int o get_default_print_depth)
+    (put_default_print_depth o Markup.parse_int)
     ProofGeneral.pgipint
     "print-depth"
     "Setting for the ML print depth";
@@ -123,7 +123,7 @@
 val _ =
   ProofGeneral.preference_option ProofGeneral.category_tracing
     NONE
-    @{option exception_trace}
+    @{option ML_exception_trace}
     "debugging"
     "Whether to enable exception trace for toplevel command execution";
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Pure/pure_syn.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -25,7 +25,7 @@
           val source = {delimited = true, text = cat_lines lines, pos = pos};
         in
           gthy
-          |> ML_Context.exec (fn () => ML_Context.eval_source true source)
+          |> ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source)
           |> Local_Theory.propagate_ml_env
           |> Context.mapping provide (Local_Theory.background_theory provide)
         end)));
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/Metis/make_metis
--- a/src/Tools/Metis/make_metis	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Tools/Metis/make_metis	Tue Mar 25 20:12:53 2014 +0100
@@ -28,8 +28,6 @@
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (******************************************************************)
 
-print_depth 0;
-
 EOF
 
   for FILE in $FILES
@@ -51,7 +49,6 @@
 
   cat <<EOF
 ;
-print_depth 10;
 EOF
 
 ) > metis.ML
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/Metis/metis.ML
--- a/src/Tools/Metis/metis.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Tools/Metis/metis.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -14,8 +14,6 @@
 (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
 (******************************************************************)
 
-print_depth 0;
-
 
 (**** Original file: src/Random.sig ****)
 
@@ -21462,4 +21460,3 @@
 
 end
 ;
-print_depth 10;
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/ROOT
--- a/src/Tools/ROOT	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Tools/ROOT	Tue Mar 25 20:12:53 2014 +0100
@@ -7,3 +7,8 @@
   theories [condition = ISABELLE_POLYML]
     Examples
 
+session SML in SML = Pure +
+  options [condition = ISABELLE_POLYML]
+  theories
+    Examples
+
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/SML/Example.sig
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/SML/Example.sig	Tue Mar 25 20:12:53 2014 +0100
@@ -0,0 +1,6 @@
+signature Example =
+sig
+  type t
+  val a: t
+  val b: t -> t
+end
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/SML/Example.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/SML/Example.sml	Tue Mar 25 20:12:53 2014 +0100
@@ -0,0 +1,9 @@
+structure Example :> Example =
+struct
+
+type t = int
+
+val a = 0
+fun b x = x + 1
+
+end
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/SML/Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/SML/Examples.thy	Tue Mar 25 20:12:53 2014 +0100
@@ -0,0 +1,37 @@
+(*  Title:      Tools/SML/Examples.thy
+    Author:     Makarius
+*)
+
+header {* Standard ML within the Isabelle environment *}
+
+theory Examples
+imports Pure
+begin
+
+text {*
+  Isabelle/ML is a somewhat augmented version of Standard ML, with
+  various add-ons that are indispensable for Isabelle development, but
+  may cause conflicts with independent projects in plain Standard ML.
+
+  The Isabelle/Isar command 'SML_file' supports official Standard ML
+  within the Isabelle environment, with full support in the Prover IDE
+  (Isabelle/jEdit).
+
+  Here is a very basic example that defines the factorial function and
+  evaluates it for some arguments.
+*}
+
+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
+  environment is enriched cumulatively within the theory context of
+  Isabelle --- independently of the Isabelle/ML environment.
+*}
+
+SML_file "Example.sig"
+SML_file "Example.sml"
+
+end
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/SML/factorial.sml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/SML/factorial.sml	Tue Mar 25 20:12:53 2014 +0100
@@ -0,0 +1,6 @@
+fun factorial 0 = 1
+  | factorial n = n * factorial (n - 1);
+
+factorial 10;
+factorial 100;
+factorial 1000;
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Mar 25 20:12:53 2014 +0100
@@ -61,6 +61,7 @@
   "src/modes/isabelle-options.xml"
   "src/modes/isabelle-root.xml"
   "src/modes/isabelle.xml"
+  "src/modes/sml.xml"
 )
 
 
@@ -277,9 +278,7 @@
   cp -p -R -f src/modes/. dist/modes/.
 
   perl -i -e 'while (<>) {
-    if (m/FILE_NAME_GLOB="\*\.{sml,ml}"/) {
-      print qq,\t\t\t\tFILE_NAME_GLOB="*.sml" />\n,;
-    }
+    if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="\*\.{sml,ml}"/) { }
     elsif (m/NAME="javacc"/) {
       print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;
       print qq,<MODE NAME="isabelle-ml" FILE="isabelle-ml.xml" FILE_NAME_GLOB="*.ML"/>\n\n,;
@@ -288,6 +287,10 @@
       print qq,<MODE NAME="isabelle-root" FILE="isabelle-root.xml" FILE_NAME_GLOB="ROOT"/>\n\n,;
       print;
     }
+    elsif (m/NAME="sqr"/) {
+      print qq!<MODE NAME="sml" FILE="sml.xml" FILE_NAME_GLOB="*.{sml,sig}"/>\n\n!;
+      print;
+    }
     else { print; }
   }' dist/modes/catalog
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Mar 25 20:12:53 2014 +0100
@@ -29,12 +29,17 @@
       "isabelle-news",    // NEWS
       "isabelle-options", // etc/options
       "isabelle-output",  // pretty text area output
-      "isabelle-root")    // session ROOT
+      "isabelle-root",    // session ROOT
+      "sml")              // Standard ML (not Isabelle/ML)
 
   private lazy val ml_syntax: Outer_Syntax =
     Outer_Syntax.init().no_tokens.
       set_language_context(Completion.Language_Context.ML_outer)
 
+  private lazy val sml_syntax: Outer_Syntax =
+    Outer_Syntax.init().no_tokens.
+      set_language_context(Completion.Language_Context.SML_outer)
+
   private lazy val news_syntax: Outer_Syntax =
     Outer_Syntax.init().no_tokens
 
@@ -48,6 +53,7 @@
       case "isabelle-ml" => Some(ml_syntax)
       case "isabelle-news" => Some(news_syntax)
       case "isabelle-output" => None
+      case "sml" => Some(sml_syntax)
       case _ => None
     }
 
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/jEdit/src/modes/sml.xml
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/modes/sml.xml	Tue Mar 25 20:12:53 2014 +0100
@@ -0,0 +1,15 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE MODE SYSTEM "xmode.dtd">
+
+<!-- Standard ML mode -->
+<MODE>
+  <PROPS>
+    <PROPERTY NAME="commentStart" VALUE="(*"/>
+    <PROPERTY NAME="commentEnd" VALUE="*)"/>
+    <PROPERTY NAME="noWordSep" VALUE="_'."/>
+    <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+    <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
+    <PROPERTY NAME="tabSize" VALUE="2" />
+    <PROPERTY NAME="indentSize" VALUE="2" />
+  </PROPS>
+</MODE>
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Mar 25 20:12:53 2014 +0100
@@ -681,7 +681,9 @@
       Markup.ML_NUMERAL -> inner_numeral_color,
       Markup.ML_CHAR -> inner_quoted_color,
       Markup.ML_STRING -> inner_quoted_color,
-      Markup.ML_COMMENT -> inner_comment_color)
+      Markup.ML_COMMENT -> inner_comment_color,
+      Markup.SML_STRING -> inner_quoted_color,
+      Markup.SML_COMMENT -> inner_comment_color)
 
   private lazy val text_color_elements =
     Document.Elements(text_colors.keySet)
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Mar 25 20:12:53 2014 +0100
@@ -203,8 +203,8 @@
       val context1 =
       {
         val (styled_tokens, context1) =
-          if (mode == "isabelle-ml") {
-            val (tokens, ctxt1) = ML_Lex.tokenize_line(line, line_ctxt.get)
+          if (mode == "isabelle-ml" || mode == "sml") {
+            val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, line_ctxt.get)
             val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
             (styled_tokens, new Line_Context(Some(ctxt1)))
           }
diff -r def3bbe6f2a5 -r fc4cf41d3504 src/ZF/Tools/twos_compl.ML
--- a/src/ZF/Tools/twos_compl.ML	Tue Mar 25 14:20:58 2014 +0100
+++ b/src/ZF/Tools/twos_compl.ML	Tue Mar 25 20:12:53 2014 +0100
@@ -15,9 +15,6 @@
 For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
 
 Still needs division!
-
-print_depth 40;
-System.Control.Print.printDepth := 350; 
 *)
 
 infix 5 $$ $$$