--- a/Admin/components/components.sha1 Thu Sep 26 08:44:43 2013 -0700
+++ b/Admin/components/components.sha1 Thu Sep 26 23:27:09 2013 +0200
@@ -37,6 +37,7 @@
5de3e399be2507f684b49dfd13da45228214bbe4 jedit_build-20130905.tar.gz
87136818fd5528d97288f5b06bd30c787229eb0d jedit_build-20130910.tar.gz
c63189cbe39eb8104235a0928f579d9523de78a9 jedit_build-20130925.tar.gz
+65cc13054be20d3a60474d406797c32a976d7db7 jedit_build-20130926.tar.gz
0bd2bc2d9a491ba5fc8dd99df27c04f11a72e8fa jfreechart-1.0.14-1.tar.gz
8122526f1fc362ddae1a328bdbc2152853186fee jfreechart-1.0.14.tar.gz
6c737137cc597fc920943783382e928ea79e3feb kodkodi-1.2.16.tar.gz
--- a/Admin/components/main Thu Sep 26 08:44:43 2013 -0700
+++ b/Admin/components/main Thu Sep 26 23:27:09 2013 +0200
@@ -4,7 +4,7 @@
exec_process-1.0.3
Haskabelle-2013
jdk-7u40
-jedit_build-20130925
+jedit_build-20130926
jfreechart-1.0.14-1
kodkodi-1.5.2
polyml-5.5.1
--- a/Admin/lib/Tools/makedist_bundle Thu Sep 26 08:44:43 2013 -0700
+++ b/Admin/lib/Tools/makedist_bundle Thu Sep 26 23:27:09 2013 +0200
@@ -170,6 +170,7 @@
mv "$ISABELLE_TARGET/contrib/macos_app" "$TMP/."
perl -pi \
+ -e 's,\Qaction-bar.shortcut=C+ENTER\E,action-bar.shortcut=\naction-bar.shortcut2=C+ENTER,g;' \
-e "s,lookAndFeel=.*,lookAndFeel=com.apple.laf.AquaLookAndFeel,g;" \
-e "s,delete-line.shortcut=.*,delete-line.shortcut=C+d,g;" \
-e "s,delete.shortcut2=.*,delete.shortcut2=A+d,g;" \
--- a/src/HOL/ROOT Thu Sep 26 08:44:43 2013 -0700
+++ b/src/HOL/ROOT Thu Sep 26 23:27:09 2013 +0200
@@ -560,6 +560,7 @@
IArray_Examples
SVC_Oracle
Simps_Case_Conv_Examples
+ ML
theories [skip_proofs = false]
Meson_Test
theories [condition = SVC_HOME]
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/ML.thy Thu Sep 26 23:27:09 2013 +0200
@@ -0,0 +1,136 @@
+(* Title: HOL/ex/ML.thy
+ Author: Makarius
+*)
+
+header {* Isabelle/ML basics *}
+
+theory "ML"
+imports Main
+begin
+
+section {* ML expressions *}
+
+text {*
+ The Isabelle command 'ML' allows to embed Isabelle/ML source into the formal
+ text. It is type-checked, compiled, and run within that environment.
+
+ Note that side-effects should be avoided, unless the intention is to change
+ global parameters of the run-time environment (rare).
+
+ ML top-level bindings are managed within the theory context.
+*}
+
+ML {* 1 + 1 *}
+
+ML {* val a = 1 *}
+ML {* val b = 1 *}
+ML {* val c = a + b *}
+
+
+section {* Antiquotations *}
+
+text {* There are some language extensions (via antiquotations), as explained in
+ the "Isabelle/Isar implementation manual", chapter 0. *}
+
+ML {* length [] *}
+ML {* @{assert} (length [] = 0) *}
+
+
+text {* Formal entities from the surrounding context may be referenced as
+ follows: *}
+
+term "1 + 1" -- "term within theory source"
+
+ML {*
+ @{term "1 + 1"} (* term as symbolic ML datatype value *)
+*}
+
+ML {*
+ @{term "1 + (1::int)"}
+*}
+
+
+section {* IDE support *}
+
+text {*
+ ML embedded into the Isabelle environment is connected to the Prover IDE.
+ Poly/ML provides:
+ \<bullet> precise positions for warnings / errors
+ \<bullet> markup for defining positions of identifiers
+ \<bullet> markup for inferred types of sub-expressions
+*}
+
+ML {* fn i => fn list => length list + i *}
+
+
+section {* Example: factorial and ackermann function in Isabelle/ML *}
+
+ML {*
+ fun factorial 0 = 1
+ | factorial n = n * factorial (n - 1)
+*}
+
+ML "factorial 42"
+ML "factorial 10000 div factorial 9999"
+
+text {*
+ See http://mathworld.wolfram.com/AckermannFunction.html
+*}
+
+ML {*
+ fun ackermann 0 n = n + 1
+ | ackermann m 0 = ackermann (m - 1) 1
+ | ackermann m n = ackermann (m - 1) (ackermann m (n - 1))
+*}
+
+ML {* timeit (fn () => ackermann 3 10) *}
+
+
+section {* Parallel Isabelle/ML *}
+
+text {*
+ Future.fork/join/cancel manage parallel evaluation.
+
+ Note that within Isabelle theory documents, the top-level command boundary may
+ not be transgressed without special precautions. This is normally managed by
+ the system when performing parallel proof checking. *}
+
+ML {*
+ val x = Future.fork (fn () => ackermann 3 10);
+ val y = Future.fork (fn () => ackermann 3 10);
+ val z = Future.join x + Future.join y
+*}
+
+text {*
+ The @{ML_struct Par_List} module provides high-level combinators for
+ parallel list operations. *}
+
+ML {* timeit (fn () => map (fn n => ackermann 3 n) (1 upto 10)) *}
+ML {* timeit (fn () => Par_List.map (fn n => ackermann 3 n) (1 upto 10)) *}
+
+
+section {* Function specifications in Isabelle/HOL *}
+
+fun factorial :: "nat \<Rightarrow> nat"
+where
+ "factorial 0 = 1"
+| "factorial (Suc n) = Suc n * factorial n"
+
+term "factorial 4" -- "symbolic term"
+value "factorial 4" -- "evaluation via ML code generation in the background"
+
+declare [[ML_trace]]
+ML {* @{term "factorial 4"} *} -- "symbolic term in ML"
+ML {* @{code "factorial"} *} -- "ML code from function specification"
+
+
+fun ackermann :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+ "ackermann 0 n = n + 1"
+| "ackermann (Suc m) 0 = ackermann m 1"
+| "ackermann (Suc m) (Suc n) = ackermann m (ackermann (Suc m) n)"
+
+value "ackermann 3 5"
+
+end
+
--- a/src/Pure/Tools/doc.scala Thu Sep 26 08:44:43 2013 -0700
+++ b/src/Pure/Tools/doc.scala Thu Sep 26 23:27:09 2013 +0200
@@ -59,6 +59,7 @@
val names =
List(
"src/HOL/ex/Seq.thy",
+ "src/HOL/ex/ML.thy",
"src/HOL/Unix/Unix.thy",
"src/HOL/Isar_Examples/Drinker.thy")
Section("Examples") :: names.map(name => text_file(name).get)
--- a/src/Tools/jEdit/patches/brackets Thu Sep 26 08:44:43 2013 -0700
+++ b/src/Tools/jEdit/patches/brackets Thu Sep 26 23:27:09 2013 +0200
@@ -1,3 +1,17 @@
+diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java
+--- 5.1.0/jEdit/org/gjt/sp/jedit/textarea/TextArea.java 2013-07-28 19:03:32.000000000 +0200
++++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/textarea/TextArea.java 2013-09-26 16:09:50.131780476 +0200
+@@ -1610,8 +1615,8 @@
+ }
+
+ // Scan backwards, trying to find a bracket
+- String openBrackets = "([{";
+- String closeBrackets = ")]}";
++ String openBrackets = "([{«‹⟨⌈⌊⦇⟦⦃";
++ String closeBrackets = ")]}»›⟩⌉⌋⦈⟧⦄'";
+ int count = 1;
+ char openBracket = '\0';
+ char closeBracket = '\0';
diff -ru 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java
--- 5.1.0/jEdit/org/gjt/sp/jedit/TextUtilities.java 2013-07-28 19:03:24.000000000 +0200
+++ 5.1.0/jEdit-patched/org/gjt/sp/jedit/TextUtilities.java 2013-09-05 10:51:09.996193290 +0200
--- a/src/Tools/jEdit/src/jEdit.props Thu Sep 26 08:44:43 2013 -0700
+++ b/src/Tools/jEdit/src/jEdit.props Thu Sep 26 23:27:09 2013 +0200
@@ -1,4 +1,5 @@
#jEdit properties
+action-bar.shortcut=C+ENTER
buffer.deepIndent=false
buffer.encoding=UTF-8-Isabelle
buffer.indentSize=2
--- a/src/Tools/jEdit/src/modes/isabelle-news.xml Thu Sep 26 08:44:43 2013 -0700
+++ b/src/Tools/jEdit/src/modes/isabelle-news.xml Thu Sep 26 23:27:09 2013 +0200
@@ -5,8 +5,8 @@
<MODE>
<PROPS>
<PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
--- a/src/Tools/jEdit/src/modes/isabelle-options.xml Thu Sep 26 08:44:43 2013 -0700
+++ b/src/Tools/jEdit/src/modes/isabelle-options.xml Thu Sep 26 23:27:09 2013 +0200
@@ -4,9 +4,11 @@
<!-- Isabelle options 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="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
--- a/src/Tools/jEdit/src/modes/isabelle-root.xml Thu Sep 26 08:44:43 2013 -0700
+++ b/src/Tools/jEdit/src/modes/isabelle-root.xml Thu Sep 26 23:27:09 2013 +0200
@@ -4,9 +4,11 @@
<!-- Isabelle session root 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="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
--- a/src/Tools/jEdit/src/modes/isabelle.xml Thu Sep 26 08:44:43 2013 -0700
+++ b/src/Tools/jEdit/src/modes/isabelle.xml Thu Sep 26 23:27:09 2013 +0200
@@ -7,27 +7,9 @@
<PROPERTY NAME="commentStart" VALUE="(*"/>
<PROPERTY NAME="commentEnd" VALUE="*)"/>
<PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE="›»)]}" />
+ <PROPERTY NAME="unalignedOpenBrackets" VALUE="{[(«‹⟨⌈⌊⦇⟦⦃" />
+ <PROPERTY NAME="unalignedCloseBrackets" VALUE="⦄⟧⦈⌋⌉⟩›»)]}" />
<PROPERTY NAME="tabSize" VALUE="2" />
<PROPERTY NAME="indentSize" VALUE="2" />
</PROPS>
- <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
- <SPAN TYPE="COMMENT1">
- <BEGIN>(*</BEGIN>
- <END>*)</END>
- </SPAN>
- <SPAN TYPE="COMMENT3">
- <BEGIN>{*</BEGIN>
- <END>*}</END>
- </SPAN>
- <SPAN TYPE="LITERAL1">
- <BEGIN>`</BEGIN>
- <END>`</END>
- </SPAN>
- <SPAN TYPE="LITERAL3">
- <BEGIN>"</BEGIN>
- <END>"</END>
- </SPAN>
- </RULES>
</MODE>