--- a/doc-src/IsarImplementation/Thy/ML.thy Thu Oct 28 12:33:24 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Thu Oct 28 15:10:34 2010 +0200
@@ -463,7 +463,7 @@
\end{enumerate}
Such weakly structured layout should be use with great care. Here
- is a counter-example involving @{ML_text let} expressions:
+ are some counter-examples involving @{ML_text let} expressions:
\begin{verbatim}
(* WRONG *)
@@ -472,6 +472,10 @@
val y = ...
in ... end
+ fun foo x = let
+ val y = ...
+ in ... end
+
fun foo x =
let
val y = ...
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Thu Oct 28 12:33:24 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Thu Oct 28 15:10:34 2010 +0200
@@ -519,7 +519,7 @@
of this module do not care about the declaration order, since that
data structure forces its own arrangement of elements.
- Observe how the @{verbatim merge} operation joins the data slots of
+ Observe how the @{ML_text merge} operation joins the data slots of
the two constituents: @{ML Ord_List.union} prevents duplication of
common data from different branches, thus avoiding the danger of
exponential blowup. Plain list append etc.\ must never be used for
--- a/doc-src/IsarImplementation/Thy/Proof.thy Thu Oct 28 12:33:24 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Thu Oct 28 15:10:34 2010 +0200
@@ -182,7 +182,7 @@
text {* In the above example, the starting context is derived from the
toplevel theory, which means that fixed variables are internalized
- literally: @{verbatim "x"} is mapped again to @{verbatim "x"}, and
+ literally: @{text "x"} is mapped again to @{text "x"}, and
attempting to fix it again in the subsequent context is an error.
Alternatively, fixed parameters can be renamed explicitly as
follows: *}
@@ -194,7 +194,7 @@
*}
text {* The following ML code can now work with the invented names of
- @{verbatim x1}, @{verbatim x2}, @{verbatim x3}, without depending on
+ @{text x1}, @{text x2}, @{text x3}, without depending on
the details on the system policy for introducing these variants.
Recall that within a proof body the system always invents fresh
``skolem constants'', e.g.\ as follows: *}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 28 12:33:24 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Thu Oct 28 15:10:34 2010 +0200
@@ -484,7 +484,7 @@
\end{enumerate}
Such weakly structured layout should be use with great care. Here
- is a counter-example involving \verb|let| expressions:
+ are some counter-examples involving \verb|let| expressions:
\begin{verbatim}
(* WRONG *)
@@ -493,6 +493,10 @@
val y = ...
in ... end
+ fun foo x = let
+ val y = ...
+ in ... end
+
fun foo x =
let
val y = ...
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Thu Oct 28 12:33:24 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Thu Oct 28 15:10:34 2010 +0200
@@ -301,7 +301,7 @@
\begin{isamarkuptext}%
In the above example, the starting context is derived from the
toplevel theory, which means that fixed variables are internalized
- literally: \verb|x| is mapped again to \verb|x|, and
+ literally: \isa{x} is mapped again to \isa{x}, and
attempting to fix it again in the subsequent context is an error.
Alternatively, fixed parameters can be renamed explicitly as
follows:%
@@ -332,7 +332,7 @@
%
\begin{isamarkuptext}%
The following ML code can now work with the invented names of
- \verb|x1|, \verb|x2|, \verb|x3|, without depending on
+ \isa{x{\isadigit{1}}}, \isa{x{\isadigit{2}}}, \isa{x{\isadigit{3}}}, without depending on
the details on the system policy for introducing these variants.
Recall that within a proof body the system always invents fresh
``skolem constants'', e.g.\ as follows:%
--- a/src/Tools/WWW_Find/scgi_req.ML Thu Oct 28 12:33:24 2010 +0200
+++ b/src/Tools/WWW_Find/scgi_req.ML Thu Oct 28 15:10:34 2010 +0200
@@ -106,8 +106,9 @@
| SOME wv => Byte.unpackStringVec wv);
val content_length =
- (the o Int.fromString o field) "CONTENT_LENGTH"
- handle _ => raise InvalidReq "Bad CONTENT_LENGTH";
+ (case Int.fromString (field "CONTENT_LENGTH") of
+ SOME n => n
+ | NONE => raise InvalidReq "Bad CONTENT_LENGTH");
val req = Req {
path_info = field "PATH_INFO",
--- a/src/Tools/jEdit/README Thu Oct 28 12:33:24 2010 +0200
+++ b/src/Tools/jEdit/README Thu Oct 28 15:10:34 2010 +0200
@@ -55,6 +55,10 @@
Linux, but probably also the deeper reason for the other oddities of
Apple font management.
+- The native font renderer of -Dapple.awt.graphics.UseQuartz=true
+ fails to handle the infinitesimal font size of "hidden" text (e.g.
+ used in Isabelle sub/superscripts).
+
Windows/Linux
=============
--- a/src/Tools/jEdit/dist-template/etc/settings Thu Oct 28 12:33:24 2010 +0200
+++ b/src/Tools/jEdit/dist-template/etc/settings Thu Oct 28 15:10:34 2010 +0200
@@ -6,7 +6,7 @@
JEDIT_OPTIONS="-reuseview -noserver -nobackground"
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m -Xss2m -Dactors.corePoolSize=4 -Dactors.enableForkJoin=false"
#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m -Xss4m -Dactors.corePoolSize=8 -Dactors.enableForkJoin=false"
-JEDIT_SYSTEM_OPTIONS="-Dapple.awt.graphics.UseQuartz=true -Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
+JEDIT_SYSTEM_OPTIONS="-Dapple.laf.useScreenMenuBar=true -Dcom.apple.mrj.application.apple.menu.about.name=Isabelle/jEdit"
JEDIT_STYLE_SHEETS="$ISABELLE_HOME/lib/html/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css"
--- a/src/Tools/jEdit/dist-template/lib/Tools/jedit Thu Oct 28 12:33:24 2010 +0200
+++ b/src/Tools/jEdit/dist-template/lib/Tools/jedit Thu Oct 28 15:10:34 2010 +0200
@@ -106,7 +106,7 @@
if [ ! -e "$JEDIT_SETTINGS/perspective.xml" ]; then
cat > "$JEDIT_SETTINGS/DockableWindowManager/perspective-view0.xml" <<EOF
-<DOCKING LEFT="" TOP="" RIGHT="isabelle-session" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
+<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-session" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />
EOF
cat > "$JEDIT_SETTINGS/perspective.xml" <<EOF
<?xml version="1.0" encoding="UTF-8" ?>
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Thu Oct 28 12:33:24 2010 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Thu Oct 28 15:10:34 2010 +0200
@@ -178,9 +178,9 @@
insert-newline-indent.shortcut=
insert-newline.shortcut=ENTER
isabelle-output.dock-position=bottom
+isabelle-session.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
-isabelle-session.dock-position=right
line-end.shortcut=END
line-home.shortcut=HOME
lookAndFeel=com.sun.java.swing.plaf.nimbus.NimbusLookAndFeel
--- a/src/Tools/jEdit/src/jedit/document_view.scala Thu Oct 28 12:33:24 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Thu Oct 28 15:10:34 2010 +0200
@@ -130,6 +130,7 @@
private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
{
exit_popup()
+/* FIXME broken
val offset = text_area.xyToOffset(x, y)
val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
@@ -143,6 +144,7 @@
html_popup = Some(popup)
case _ =>
}
+*/
}