# HG changeset patch # User wenzelm # Date 1288271434 -7200 # Node ID 19cd739f4b0af4783c6caaa2bdd269febd46aec4 # Parent e31e3f0071d4023b15de0fd5bb6a8eb336ed6c6b# Parent ac648bedd5dca49cfcbef6ae12802cf7f82cfcf8 merged diff -r e31e3f0071d4 -r 19cd739f4b0a doc-src/IsarImplementation/Thy/ML.thy --- 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 = ... diff -r e31e3f0071d4 -r 19cd739f4b0a doc-src/IsarImplementation/Thy/Prelim.thy --- 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 diff -r e31e3f0071d4 -r 19cd739f4b0a doc-src/IsarImplementation/Thy/Proof.thy --- 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: *} diff -r e31e3f0071d4 -r 19cd739f4b0a doc-src/IsarImplementation/Thy/document/ML.tex --- 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 = ... diff -r e31e3f0071d4 -r 19cd739f4b0a doc-src/IsarImplementation/Thy/document/Proof.tex --- 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:% diff -r e31e3f0071d4 -r 19cd739f4b0a src/Tools/WWW_Find/scgi_req.ML --- 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", diff -r e31e3f0071d4 -r 19cd739f4b0a src/Tools/jEdit/README --- 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 ============= diff -r e31e3f0071d4 -r 19cd739f4b0a src/Tools/jEdit/dist-template/etc/settings --- 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" diff -r e31e3f0071d4 -r 19cd739f4b0a src/Tools/jEdit/dist-template/lib/Tools/jedit --- 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 cat > "$JEDIT_SETTINGS/perspective.xml" < diff -r e31e3f0071d4 -r 19cd739f4b0a src/Tools/jEdit/dist-template/properties/jedit.props --- 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 diff -r e31e3f0071d4 -r 19cd739f4b0a src/Tools/jEdit/src/jedit/document_view.scala --- 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 _ => } +*/ }