--- 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
--- 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
--- 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.
--- 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"
--- 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"
--- 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"
--- 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}
--- 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
--- 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) ^ "}" ^
--- 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 *}
--- 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
--- 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;
--- 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"
--- 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)))
--- 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 *)
*}
--- 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";
-*)
--- 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;
*}
--- 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"
--- 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)
--- 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 #>
--- 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;
--- 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 _ =
--- 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 ^ ")")));
--- 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 =
--- 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;
--- 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 ())))))";
--- 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 _ => \"?\")";
--- 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;
+
--- 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;
--- 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 _ =
--- 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");
--- 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,
--- 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;
--- 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)
--- 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;
--- 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";
--- 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"
--- 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
--- 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 *)
--- 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
--- 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)
}
--- 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";
--- 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)));
--- 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
--- 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;
--- 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
+
--- /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
--- /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
--- /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
--- /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;
--- 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
--- 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
}
--- /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>
--- 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)
--- 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)))
}
--- 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 $$ $$$