# HG changeset patch
# User wenzelm
# Date 1380230829 -7200
# Node ID f95765a28b1de3d80ce612be5ad751fff05524ff
# Parent  896b642f2aab594fa49c2f71cc8a356443fce37e# Parent  eed09ad6c5df5f1f60ebee99e34c2f264fe4abb1
merged

diff -r 896b642f2aab -r f95765a28b1d Admin/components/components.sha1
--- 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
diff -r 896b642f2aab -r f95765a28b1d Admin/components/main
--- 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
diff -r 896b642f2aab -r f95765a28b1d Admin/lib/Tools/makedist_bundle
--- 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;" \
diff -r 896b642f2aab -r f95765a28b1d src/HOL/ROOT
--- 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]
diff -r 896b642f2aab -r f95765a28b1d src/HOL/ex/ML.thy
--- /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
+
diff -r 896b642f2aab -r f95765a28b1d src/Pure/Tools/doc.scala
--- 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)
diff -r 896b642f2aab -r f95765a28b1d src/Tools/jEdit/patches/brackets
--- 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
diff -r 896b642f2aab -r f95765a28b1d src/Tools/jEdit/src/jEdit.props
--- 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
diff -r 896b642f2aab -r f95765a28b1d src/Tools/jEdit/src/modes/isabelle-news.xml
--- 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>
diff -r 896b642f2aab -r f95765a28b1d src/Tools/jEdit/src/modes/isabelle-options.xml
--- 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>
diff -r 896b642f2aab -r f95765a28b1d src/Tools/jEdit/src/modes/isabelle-root.xml
--- 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>
diff -r 896b642f2aab -r f95765a28b1d src/Tools/jEdit/src/modes/isabelle.xml
--- 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>