--- a/.hgtags Sun Oct 09 11:13:53 2011 +0200
+++ b/.hgtags Mon Oct 10 11:12:09 2011 +0200
@@ -27,3 +27,5 @@
6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2
6d736d983d5cfec4a6c6fba174db2cd93493a96b Isabelle2011
+76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1
+
--- a/Admin/CHECKLIST Sun Oct 09 11:13:53 2011 +0200
+++ b/Admin/CHECKLIST Mon Oct 10 11:12:09 2011 +0200
@@ -42,12 +42,12 @@
- makebin (multiplatform);
-- makebin -l on fast machine;
-
- makebundle (multiplatform);
- hdiutil create -srcfolder DIR DMG (Mac OS);
+- makebin -l on fast machine, based on renamed bundle with deleted heaps;
+
Final release stage
===================
--- a/Admin/MacOS/App1/script Sun Oct 09 11:13:53 2011 +0200
+++ b/Admin/MacOS/App1/script Mon Oct 10 11:12:09 2011 +0200
@@ -106,8 +106,7 @@
( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
RC=$?
else
- rm -f "$OUTPUT" && touch "$OUTPUT"
- "$ISABELLE_TOOL" jedit "$@"
+ ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
RC=$?
fi
--- a/Admin/build Sun Oct 09 11:13:53 2011 +0200
+++ b/Admin/build Mon Oct 10 11:12:09 2011 +0200
@@ -84,7 +84,7 @@
function build_jars ()
{
- "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
+ "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
pushd "$ISABELLE_HOME/src/Pure" >/dev/null
"$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
popd >/dev/null
--- a/Admin/makedist Sun Oct 09 11:13:53 2011 +0200
+++ b/Admin/makedist Mon Oct 10 11:12:09 2011 +0200
@@ -178,7 +178,6 @@
echo
} >ANNOUNCE
else
- rm Isabelle Isabelle.exe
perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
fi
--- a/doc-src/IsarRef/Thy/First_Order_Logic.thy Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy Mon Oct 10 11:12:09 2011 +0200
@@ -47,7 +47,7 @@
text {*
\noindent Substitution is very powerful, but also hard to control in
full generality. We derive some common symmetry~/ transitivity
- schemes of as particular consequences.
+ schemes of @{term equal} as particular consequences.
*}
theorem sym [sym]:
--- a/doc-src/IsarRef/Thy/Proof.thy Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy Mon Oct 10 11:12:09 2011 +0200
@@ -129,7 +129,7 @@
proof structure at all, but goes back right to the theory level.
Furthermore, @{command "oops"} does not produce any result theorem
--- there is no intended claim to be able to complete the proof
- anyhow.
+ in any way.
A typical application of @{command "oops"} is to explain Isar proofs
\emph{within} the system itself, in conjunction with the document
--- a/doc-src/IsarRef/Thy/Synopsis.thy Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/Synopsis.thy Mon Oct 10 11:12:09 2011 +0200
@@ -907,7 +907,7 @@
text {* There is nothing special about logical connectives (@{text
"\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.). Operators from
- set-theory or lattice-theory for analogously. It is only a matter
+ set-theory or lattice-theory work analogously. It is only a matter
of rule declarations in the library; rules can be also specified
explicitly.
*}
@@ -1105,4 +1105,4 @@
note `C`
end
-end
\ No newline at end of file
+end
--- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex Mon Oct 10 11:12:09 2011 +0200
@@ -68,7 +68,7 @@
\begin{isamarkuptext}%
\noindent Substitution is very powerful, but also hard to control in
full generality. We derive some common symmetry~/ transitivity
- schemes of as particular consequences.%
+ schemes of \isa{equal} as particular consequences.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
--- a/doc-src/IsarRef/Thy/document/Proof.tex Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Proof.tex Mon Oct 10 11:12:09 2011 +0200
@@ -159,7 +159,7 @@
proof structure at all, but goes back right to the theory level.
Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
--- there is no intended claim to be able to complete the proof
- anyhow.
+ in any way.
A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
\emph{within} the system itself, in conjunction with the document
--- a/doc-src/IsarRef/Thy/document/Synopsis.tex Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex Mon Oct 10 11:12:09 2011 +0200
@@ -2258,7 +2258,7 @@
%
\begin{isamarkuptext}%
There is nothing special about logical connectives (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} etc.). Operators from
- set-theory or lattice-theory for analogously. It is only a matter
+ set-theory or lattice-theory work analogously. It is only a matter
of rule declarations in the library; rules can be also specified
explicitly.%
\end{isamarkuptext}%
@@ -2708,6 +2708,7 @@
{\isafoldtheory}%
%
\isadelimtheory
+\isanewline
%
\endisadelimtheory
\end{isabellebody}%
--- a/doc-src/TutorialI/Documents/Documents.thy Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/TutorialI/Documents/Documents.thy Mon Oct 10 11:12:09 2011 +0200
@@ -344,7 +344,7 @@
session is derived from a single parent, usually an object-logic
image like \texttt{HOL}. This results in an overall tree structure,
which is reflected by the output location in the file system
- (usually rooted at \verb,~/.isabelle/browser_info,).
+ (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
\medskip The easiest way to manage Isabelle sessions is via
\texttt{isabelle mkdir} (generates an initial session source setup)
--- a/doc-src/TutorialI/Documents/document/Documents.tex Sun Oct 09 11:13:53 2011 +0200
+++ b/doc-src/TutorialI/Documents/document/Documents.tex Mon Oct 10 11:12:09 2011 +0200
@@ -417,7 +417,7 @@
session is derived from a single parent, usually an object-logic
image like \texttt{HOL}. This results in an overall tree structure,
which is reflected by the output location in the file system
- (usually rooted at \verb,~/.isabelle/browser_info,).
+ (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
\medskip The easiest way to manage Isabelle sessions is via
\texttt{isabelle mkdir} (generates an initial session source setup)
--- a/etc/user-settings.sample Sun Oct 09 11:13:53 2011 +0200
+++ b/etc/user-settings.sample Mon Oct 10 11:12:09 2011 +0200
@@ -1,6 +1,6 @@
# -*- shell-script -*- :mode=shellscript:
#
-# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
+# Isabelle user settings sample -- for use in $ISABELLE_HOME_USER/etc/settings
ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
ISABELLE_LOGIC=HOL
--- a/lib/Tools/java Sun Oct 09 11:13:53 2011 +0200
+++ b/lib/Tools/java Mon Oct 10 11:12:09 2011 +0200
@@ -8,6 +8,13 @@
JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
+if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then
+ :
+else
+ echo "Bad Java executable: \"$JAVA_EXE\"" >&2
+ exit 2
+fi
+
if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
SERVER="-server"
else
--- a/lib/scripts/getsettings Sun Oct 09 11:13:53 2011 +0200
+++ b/lib/scripts/getsettings Mon Oct 10 11:12:09 2011 +0200
@@ -14,7 +14,7 @@
export ISABELLE_HOME
if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
then
- echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
+ echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
fi
--- a/src/Pure/System/isabelle_system.scala Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon Oct 10 11:12:09 2011 +0200
@@ -110,6 +110,16 @@
def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
def platform_file(path: Path): File = new File(platform_path(path))
+ def platform_file_url(raw_path: Path): String =
+ {
+ val path = raw_path.expand
+ require(path.is_absolute)
+ val s = platform_path(path).replaceAll(" ", "%20")
+ if (!Platform.is_windows) "file://" + s
+ else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
+ else "file:///" + s.replace('\\', '/')
+ }
+
def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
Binary file src/Tools/jEdit/PIDE.png has changed
--- a/src/Tools/jEdit/README.html Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Tools/jEdit/README.html Mon Oct 10 11:12:09 2011 +0200
@@ -7,17 +7,43 @@
<style type="text/css" media="screen">
body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
</style>
-<title>Notes on the Isabelle/jEdit Prover IDE</title>
+<title>Welcome to the Isabelle/jEdit Prover IDE</title>
</head>
<body>
-<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
+<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
+
+<p>
+ <b>PIDE</b> is a novel framework for sophisticated Prover IDEs,
+ based on Isabelle/Scala technology that is integrated with Isabelle.
+ It is build around a concept of
+ <em>asynchronous document processing</em>, which is supported
+ natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
+</p>
+
+<p>
+ <b>Isabelle/jEdit</b> is an example application within the PIDE
+ framework — it illustrates many of the ideas in a realistic
+ manner, ready to be used right now in Isabelle applications.
+</p>
-The Isabelle/Scala layer that is already part of Isabelle/Pure
-provides some general infrastructure for advanced prover interaction
-and integration. The Isabelle/jEdit application serves as an example
-for asynchronous proof checking with support for parallel processing.
+<p>
+ <em>Research and implementation of concepts around PIDE has been
+ kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
+ Université Paris-Sud (http://www.u-psud.fr), and Digiteo
+ (http://www.digiteo.fr).</em>
+</p>
+
+
+
+<h2>The Isabelle/jEdit Prover IDE</h2>
+
+<p>
+Isabelle/jEdit consists of some plugins for the well-known jEdit text
+editor framework (http://www.jedit.org), according to the following
+principles.
+</p>
<ul>
@@ -35,18 +61,21 @@
<li>Using the mouse together with the modifier key <tt>C</tt>
(<tt>CONTROL</tt> on Linux or Windows,
- <tt>COMMAND</tt> on Mac OS) exposes additional information.</li>
+ <tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
<li>Dockable panels (e.g. <em>Output</em>) are managed as independent
windows by jEdit, which also allows multiple instances.</li>
+<li>Prover process and source files are managed by the Scala layer on
+the editor side. The prover experiences a mostly timeless and
+stateless environment of formal document content.</li>
+
</ul>
<h2>Isabelle symbols and fonts</h2>
<ul>
-
<li>Isabelle supports infinitely many symbols:<br/>
α, β, γ, …<br/>
∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
@@ -118,10 +147,16 @@
as the Unicode sequences coincide with the symbol mapping.
</li>
+ <li><b>NOTE:</b> Raw unicode characters within prover source files
+ should be restricted to informal parts, e.g. to write text in
+ non-latin alphabets. Mathematical symbols should be defined via the
+ official rendering tables.
+ </li>
+
</ul>
-<h2>Limitations and workrounds (September 2011)</h2>
+<h2>Limitations and workrounds (October 2011)</h2>
<ul>
<li>No way to start/stop prover or switch to a different logic.<br/>
@@ -158,7 +193,7 @@
</ul>
-<h2>Known problems with Mac OS</h2>
+<h2>Known problems with Mac OS X</h2>
<ul>
@@ -166,22 +201,21 @@
e.g. between the editor and the Console plugin, which is a standard
swing text box. Similar for search boxes etc.</li>
-<li>ToggleButton selected state is not rendered if window focus is
- lost, which is probably a genuine feature of the Apple
- look-and-feel.</li>
-
-<li>Font.createFont mangles the font family of non-regular fonts,
- e.g. bold. IsabelleText font files need to be installed/updated
- manually.</li>
+<li><tt>Font.createFont</tt> mangles the font family of non-regular
+ fonts, e.g. bold. IsabelleText font files need to be
+ installed/updated manually if bold versions are desired. Note that
+ this has to be repeated whenever fonts shipped with Isabelle are
+ updated!</li>
<li>Missing glyphs are collected from other fonts (like Emacs,
- Firefox). This is actually an advantage over the Oracle/Sun JVM on
- Windows or Linux, but probably also the deeper reason for the other
- oddities of Apple font management.</li>
+ Firefox). This is actually an advantage over the Oracle JVM on
+ Windows or Linux, but also the deeper reason for other oddities of
+ Apple font management.</li>
-<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
- (not enabled by default) fails to handle the infinitesimal font size
- of "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
+<li>The native font renderer
+ of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
+ enabled by default) fails to handle the infinitesimal font size of
+ "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
</ul>
@@ -191,23 +225,10 @@
<ul>
<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
- of the jEdit text area. Always use official JRE 1.6.x from
- Sun/Oracle/Apple.</li>
-
-<li>jEdit on OpenJDK is generally not supported.</li>
-
-</ul>
-
+ of the jEdit text area. Always use official JRE 1.6.x from Oracle
+ or Apple.</li>
-<h2>Known problems with Windows/Cygwin</h2>
-
-<ul>
-
-<li>Occasional session startup problems when loading a logic image
-takes too long (cf. output in "Prover Session / Syslog" panel).</li>
-
-<li>Auxiliary files of a theory (<tt>uses</tt>) cannot be loaded due
-to incompatible path notation inherited from MS-DOS.</li>
+<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>
</ul>
@@ -216,6 +237,8 @@
<ul>
+<li>Isabelle: BSD-style</li>
+
<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
--- a/src/Tools/jEdit/src/html_panel.scala Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Tools/jEdit/src/html_panel.scala Mon Oct 10 11:12:09 2011 +0200
@@ -113,7 +113,7 @@
/* internal messages */
private case class Resize(font_family: String, font_size: Int)
- private case class Render_Document(text: String)
+ private case class Render_Document(url: String, text: String)
private case class Render(body: XML.Body)
private case class Render_Sync(body: XML.Body)
private case object Refresh
@@ -151,9 +151,9 @@
def refresh() { render(current_body) }
- def render_document(text: String)
+ def render_document(url: String, text: String)
{
- val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
+ val doc = builder.parse(new InputSourceImpl(new StringReader(text), url))
Swing_Thread.later { setDocument(doc, rcontext) }
}
@@ -183,7 +183,7 @@
react {
case Resize(font_family, font_size) => resize(font_family, font_size)
case Refresh => refresh()
- case Render_Document(text) => render_document(text)
+ case Render_Document(url, text) => render_document(url, text)
case Render(body) => render(body)
case Render_Sync(body) => render(body); reply(())
case bad => System.err.println("main_actor: ignoring bad message " + bad)
@@ -196,7 +196,7 @@
def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
def refresh() { main_actor ! Refresh }
- def render_document(text: String) { main_actor ! Render_Document(text) }
+ def render_document(url: String, text: String) { main_actor ! Render_Document(url, text) }
def render(body: XML.Body) { main_actor ! Render(body) }
def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
}
--- a/src/Tools/jEdit/src/session_dockable.scala Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Mon Oct 10 11:12:09 2011 +0200
@@ -27,7 +27,10 @@
/* main tabs */
private val readme = new HTML_Panel("SansSerif", 14)
- readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
+ private val readme_path = Path.explode("$JEDIT_HOME/README.html")
+ readme.render_document(
+ Isabelle_System.platform_file_url(readme_path),
+ Isabelle_System.try_read(List(readme_path)))
val status = new ListView(Nil: List[Document.Node.Name]) {
listenTo(mouse.clicks)
--- a/src/Tools/subtyping.ML Sun Oct 09 11:13:53 2011 +0200
+++ b/src/Tools/subtyping.ML Mon Oct 10 11:12:09 2011 +0200
@@ -628,7 +628,7 @@
NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^
" is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))
| SOME (co, _) => co)
- | ((Type (a, Ts)), (Type (b, Us))) =>
+ | (T1 as Type (a, Ts), T2 as Type (b, Us)) =>
if a <> b
then
(case Symreltab.lookup (coes_of ctxt) (a, b) of
@@ -656,8 +656,11 @@
| ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
in
(case Symtab.lookup (tmaps_of ctxt) a of
- NONE => raise COERCION_GEN_ERROR
- (err ++> "No map function for " ^ quote a ^ " known")
+ NONE =>
+ if Type.could_unify (T1, T2)
+ then Abs (Name.uu, T1, Bound 0)
+ else raise COERCION_GEN_ERROR
+ (err ++> "No map function for " ^ quote a ^ " known")
| SOME tmap =>
let
val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));