merged
authorwenzelm
Mon Oct 10 11:12:09 2011 +0200 (2011-10-10 ago)
changeset 45124d78ec6c10fa1
parent 45122 49e305100097
parent 45123 414b083058e4
child 45125 c15b0faeb70a
merged
Admin/makedist
     1.1 --- a/.hgtags	Sun Oct 09 11:13:53 2011 +0200
     1.2 +++ b/.hgtags	Mon Oct 10 11:12:09 2011 +0200
     1.3 @@ -27,3 +27,5 @@
     1.4  6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1
     1.5  35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2
     1.6  6d736d983d5cfec4a6c6fba174db2cd93493a96b Isabelle2011
     1.7 +76fef3e570043b84a32716b5633085d2fb215525 Isabelle2011-1
     1.8 +
     2.1 --- a/Admin/CHECKLIST	Sun Oct 09 11:13:53 2011 +0200
     2.2 +++ b/Admin/CHECKLIST	Mon Oct 10 11:12:09 2011 +0200
     2.3 @@ -42,12 +42,12 @@
     2.4  
     2.5  - makebin (multiplatform);
     2.6  
     2.7 -- makebin -l on fast machine;
     2.8 -
     2.9  - makebundle (multiplatform);
    2.10  
    2.11  - hdiutil create -srcfolder DIR DMG (Mac OS);
    2.12  
    2.13 +- makebin -l on fast machine, based on renamed bundle with deleted heaps;
    2.14 +
    2.15  
    2.16  Final release stage
    2.17  ===================
     3.1 --- a/Admin/MacOS/App1/script	Sun Oct 09 11:13:53 2011 +0200
     3.2 +++ b/Admin/MacOS/App1/script	Mon Oct 10 11:12:09 2011 +0200
     3.3 @@ -106,8 +106,7 @@
     3.4    ( "$ISABELLE_TOOL" emacs "${EMACS_OPTIONS[@]}" "$@" ) > "$OUTPUT" 2>&1
     3.5    RC=$?
     3.6  else
     3.7 -  rm -f "$OUTPUT" && touch "$OUTPUT"
     3.8 -  "$ISABELLE_TOOL" jedit "$@"
     3.9 +  ( "$ISABELLE_TOOL" jedit "$@" ) > "$OUTPUT" 2>&1
    3.10    RC=$?
    3.11  fi
    3.12  
     4.1 --- a/Admin/build	Sun Oct 09 11:13:53 2011 +0200
     4.2 +++ b/Admin/build	Mon Oct 10 11:12:09 2011 +0200
     4.3 @@ -84,7 +84,7 @@
     4.4  
     4.5  function build_jars ()
     4.6  {
     4.7 -  "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
     4.8 +  "$ISABELLE_TOOL" env "$ISABELLE_HOME/lib/scripts/java_ext_dirs" >/dev/null
     4.9    pushd "$ISABELLE_HOME/src/Pure" >/dev/null
    4.10    "$ISABELLE_TOOL" env ./build-jars "$@" || exit $?
    4.11    popd >/dev/null
     5.1 --- a/Admin/makedist	Sun Oct 09 11:13:53 2011 +0200
     5.2 +++ b/Admin/makedist	Mon Oct 10 11:12:09 2011 +0200
     5.3 @@ -178,7 +178,6 @@
     5.4      echo
     5.5    } >ANNOUNCE
     5.6  else
     5.7 -  rm Isabelle Isabelle.exe
     5.8    perl -pi -e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML
     5.9  fi
    5.10  
     6.1 --- a/doc-src/IsarRef/Thy/First_Order_Logic.thy	Sun Oct 09 11:13:53 2011 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/First_Order_Logic.thy	Mon Oct 10 11:12:09 2011 +0200
     6.3 @@ -47,7 +47,7 @@
     6.4  text {*
     6.5    \noindent Substitution is very powerful, but also hard to control in
     6.6    full generality.  We derive some common symmetry~/ transitivity
     6.7 -  schemes of as particular consequences.
     6.8 +  schemes of @{term equal} as particular consequences.
     6.9  *}
    6.10  
    6.11  theorem sym [sym]:
     7.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Sun Oct 09 11:13:53 2011 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Mon Oct 10 11:12:09 2011 +0200
     7.3 @@ -129,7 +129,7 @@
     7.4    proof structure at all, but goes back right to the theory level.
     7.5    Furthermore, @{command "oops"} does not produce any result theorem
     7.6    --- there is no intended claim to be able to complete the proof
     7.7 -  anyhow.
     7.8 +  in any way.
     7.9  
    7.10    A typical application of @{command "oops"} is to explain Isar proofs
    7.11    \emph{within} the system itself, in conjunction with the document
     8.1 --- a/doc-src/IsarRef/Thy/Synopsis.thy	Sun Oct 09 11:13:53 2011 +0200
     8.2 +++ b/doc-src/IsarRef/Thy/Synopsis.thy	Mon Oct 10 11:12:09 2011 +0200
     8.3 @@ -907,7 +907,7 @@
     8.4  
     8.5  text {* There is nothing special about logical connectives (@{text
     8.6    "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.).  Operators from
     8.7 -  set-theory or lattice-theory for analogously.  It is only a matter
     8.8 +  set-theory or lattice-theory work analogously.  It is only a matter
     8.9    of rule declarations in the library; rules can be also specified
    8.10    explicitly.
    8.11  *}
    8.12 @@ -1105,4 +1105,4 @@
    8.13    note `C`
    8.14  end
    8.15  
    8.16 -end
    8.17 \ No newline at end of file
    8.18 +end
     9.1 --- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Sun Oct 09 11:13:53 2011 +0200
     9.2 +++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex	Mon Oct 10 11:12:09 2011 +0200
     9.3 @@ -68,7 +68,7 @@
     9.4  \begin{isamarkuptext}%
     9.5  \noindent Substitution is very powerful, but also hard to control in
     9.6    full generality.  We derive some common symmetry~/ transitivity
     9.7 -  schemes of as particular consequences.%
     9.8 +  schemes of \isa{equal} as particular consequences.%
     9.9  \end{isamarkuptext}%
    9.10  \isamarkuptrue%
    9.11  \isacommand{theorem}\isamarkupfalse%
    10.1 --- a/doc-src/IsarRef/Thy/document/Proof.tex	Sun Oct 09 11:13:53 2011 +0200
    10.2 +++ b/doc-src/IsarRef/Thy/document/Proof.tex	Mon Oct 10 11:12:09 2011 +0200
    10.3 @@ -159,7 +159,7 @@
    10.4    proof structure at all, but goes back right to the theory level.
    10.5    Furthermore, \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} does not produce any result theorem
    10.6    --- there is no intended claim to be able to complete the proof
    10.7 -  anyhow.
    10.8 +  in any way.
    10.9  
   10.10    A typical application of \hyperlink{command.oops}{\mbox{\isa{\isacommand{oops}}}} is to explain Isar proofs
   10.11    \emph{within} the system itself, in conjunction with the document
    11.1 --- a/doc-src/IsarRef/Thy/document/Synopsis.tex	Sun Oct 09 11:13:53 2011 +0200
    11.2 +++ b/doc-src/IsarRef/Thy/document/Synopsis.tex	Mon Oct 10 11:12:09 2011 +0200
    11.3 @@ -2258,7 +2258,7 @@
    11.4  %
    11.5  \begin{isamarkuptext}%
    11.6  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
    11.7 -  set-theory or lattice-theory for analogously.  It is only a matter
    11.8 +  set-theory or lattice-theory work analogously.  It is only a matter
    11.9    of rule declarations in the library; rules can be also specified
   11.10    explicitly.%
   11.11  \end{isamarkuptext}%
   11.12 @@ -2708,6 +2708,7 @@
   11.13  {\isafoldtheory}%
   11.14  %
   11.15  \isadelimtheory
   11.16 +\isanewline
   11.17  %
   11.18  \endisadelimtheory
   11.19  \end{isabellebody}%
    12.1 --- a/doc-src/TutorialI/Documents/Documents.thy	Sun Oct 09 11:13:53 2011 +0200
    12.2 +++ b/doc-src/TutorialI/Documents/Documents.thy	Mon Oct 10 11:12:09 2011 +0200
    12.3 @@ -344,7 +344,7 @@
    12.4    session is derived from a single parent, usually an object-logic
    12.5    image like \texttt{HOL}.  This results in an overall tree structure,
    12.6    which is reflected by the output location in the file system
    12.7 -  (usually rooted at \verb,~/.isabelle/browser_info,).
    12.8 +  (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
    12.9  
   12.10    \medskip The easiest way to manage Isabelle sessions is via
   12.11    \texttt{isabelle mkdir} (generates an initial session source setup)
    13.1 --- a/doc-src/TutorialI/Documents/document/Documents.tex	Sun Oct 09 11:13:53 2011 +0200
    13.2 +++ b/doc-src/TutorialI/Documents/document/Documents.tex	Mon Oct 10 11:12:09 2011 +0200
    13.3 @@ -417,7 +417,7 @@
    13.4    session is derived from a single parent, usually an object-logic
    13.5    image like \texttt{HOL}.  This results in an overall tree structure,
    13.6    which is reflected by the output location in the file system
    13.7 -  (usually rooted at \verb,~/.isabelle/browser_info,).
    13.8 +  (usually rooted at \verb,~/.isabelle/IsabelleXXXX/browser_info,).
    13.9  
   13.10    \medskip The easiest way to manage Isabelle sessions is via
   13.11    \texttt{isabelle mkdir} (generates an initial session source setup)
    14.1 --- a/etc/user-settings.sample	Sun Oct 09 11:13:53 2011 +0200
    14.2 +++ b/etc/user-settings.sample	Mon Oct 10 11:12:09 2011 +0200
    14.3 @@ -1,6 +1,6 @@
    14.4  # -*- shell-script -*- :mode=shellscript:
    14.5  #
    14.6 -# Isabelle user settings sample -- for use in ~/.isabelle/etc/settings
    14.7 +# Isabelle user settings sample -- for use in $ISABELLE_HOME_USER/etc/settings
    14.8  
    14.9  ISABELLE_USEDIR_OPTIONS="-i true -d pdf"
   14.10  ISABELLE_LOGIC=HOL
    15.1 --- a/lib/Tools/java	Sun Oct 09 11:13:53 2011 +0200
    15.2 +++ b/lib/Tools/java	Mon Oct 10 11:12:09 2011 +0200
    15.3 @@ -8,6 +8,13 @@
    15.4  
    15.5  JAVA_EXE="${THIS_JAVA:-$ISABELLE_JAVA}"
    15.6  
    15.7 +if "$JAVA_EXE" -version >/dev/null 2>/dev/null; then
    15.8 +  :
    15.9 +else
   15.10 +  echo "Bad Java executable: \"$JAVA_EXE\"" >&2
   15.11 +  exit 2
   15.12 +fi
   15.13 +
   15.14  if "$JAVA_EXE" -server >/dev/null 2>/dev/null; then
   15.15    SERVER="-server"
   15.16  else
    16.1 --- a/lib/scripts/getsettings	Sun Oct 09 11:13:53 2011 +0200
    16.2 +++ b/lib/scripts/getsettings	Mon Oct 10 11:12:09 2011 +0200
    16.3 @@ -14,7 +14,7 @@
    16.4  export ISABELLE_HOME
    16.5  if { echo -n "$ISABELLE_HOME" | fgrep " " >/dev/null; }
    16.6  then
    16.7 -  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems later on!"
    16.8 +  echo 1>&2 "### White space in ISABELLE_HOME may cause strange problems!"
    16.9    echo 1>&2 "### ISABELLE_HOME=\"$ISABELLE_HOME\""
   16.10  fi
   16.11  
    17.1 --- a/src/Pure/System/isabelle_system.scala	Sun Oct 09 11:13:53 2011 +0200
    17.2 +++ b/src/Pure/System/isabelle_system.scala	Mon Oct 10 11:12:09 2011 +0200
    17.3 @@ -110,6 +110,16 @@
    17.4    def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
    17.5    def platform_file(path: Path): File = new File(platform_path(path))
    17.6  
    17.7 +  def platform_file_url(raw_path: Path): String =
    17.8 +  {
    17.9 +    val path = raw_path.expand
   17.10 +    require(path.is_absolute)
   17.11 +    val s = platform_path(path).replaceAll(" ", "%20")
   17.12 +    if (!Platform.is_windows) "file://" + s
   17.13 +    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
   17.14 +    else "file:///" + s.replace('\\', '/')
   17.15 +  }
   17.16 +
   17.17    def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
   17.18  
   17.19  
    18.1 Binary file src/Tools/jEdit/PIDE.png has changed
    19.1 --- a/src/Tools/jEdit/README.html	Sun Oct 09 11:13:53 2011 +0200
    19.2 +++ b/src/Tools/jEdit/README.html	Mon Oct 10 11:12:09 2011 +0200
    19.3 @@ -7,17 +7,43 @@
    19.4  <style type="text/css" media="screen">
    19.5  body { font-family: STIXGeneral, IsabelleText; font-size: 14pt; }
    19.6  </style>
    19.7 -<title>Notes on the Isabelle/jEdit Prover IDE</title>
    19.8 +<title>Welcome to the Isabelle/jEdit Prover IDE</title>
    19.9  </head>
   19.10  
   19.11  <body>
   19.12  
   19.13 -<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
   19.14 +<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
   19.15 +
   19.16 +<p>
   19.17 +  <b>PIDE</b> is a novel framework for sophisticated Prover IDEs,
   19.18 +  based on Isabelle/Scala technology that is integrated with Isabelle.
   19.19 +  It is build around a concept of
   19.20 +  <em>asynchronous document processing</em>, which is supported
   19.21 +  natively by the <em>parallel proof engine</em> implemented in Isabelle/ML.
   19.22 +</p>
   19.23 +
   19.24 +<p>
   19.25 +  <b>Isabelle/jEdit</b> is an example application within the PIDE
   19.26 +  framework &mdash; it illustrates many of the ideas in a realistic
   19.27 +  manner, ready to be used right now in Isabelle applications.
   19.28 +</p>
   19.29  
   19.30 -The Isabelle/Scala layer that is already part of Isabelle/Pure
   19.31 -provides some general infrastructure for advanced prover interaction
   19.32 -and integration.  The Isabelle/jEdit application serves as an example
   19.33 -for asynchronous proof checking with support for parallel processing.
   19.34 +<p>
   19.35 +  <em>Research and implementation of concepts around PIDE has been
   19.36 +  kindly supported in the past 3 years by BMBF (http://www.bmbf.de),
   19.37 +  Université Paris-Sud (http://www.u-psud.fr), and Digiteo
   19.38 +  (http://www.digiteo.fr).</em>
   19.39 +</p>
   19.40 +
   19.41 +
   19.42 +
   19.43 +<h2>The Isabelle/jEdit Prover IDE</h2>
   19.44 +
   19.45 +<p>
   19.46 +Isabelle/jEdit consists of some plugins for the well-known jEdit text
   19.47 +editor framework (http://www.jedit.org), according to the following
   19.48 +principles.
   19.49 +</p>
   19.50  
   19.51  <ul>
   19.52  
   19.53 @@ -35,18 +61,21 @@
   19.54  
   19.55  <li>Using the mouse together with the modifier key <tt>C</tt>
   19.56  (<tt>CONTROL</tt> on Linux or Windows,
   19.57 -  <tt>COMMAND</tt> on Mac OS) exposes additional information.</li>
   19.58 +  <tt>COMMAND</tt> on Mac OS X) exposes additional information.</li>
   19.59  
   19.60  <li>Dockable panels (e.g. <em>Output</em>) are managed as independent
   19.61    windows by jEdit, which also allows multiple instances.</li>
   19.62  
   19.63 +<li>Prover process and source files are managed by the Scala layer on
   19.64 +the editor side.  The prover experiences a mostly timeless and
   19.65 +stateless environment of formal document content.</li>
   19.66 +
   19.67  </ul>
   19.68  
   19.69  
   19.70  <h2>Isabelle symbols and fonts</h2>
   19.71  
   19.72  <ul>
   19.73 -
   19.74    <li>Isabelle supports infinitely many symbols:<br/>
   19.75      α, β, γ, …<br/>
   19.76      ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
   19.77 @@ -118,10 +147,16 @@
   19.78      as the Unicode sequences coincide with the symbol mapping.
   19.79    </li>
   19.80  
   19.81 +  <li><b>NOTE:</b> Raw unicode characters within prover source files
   19.82 +  should be restricted to informal parts, e.g. to write text in
   19.83 +  non-latin alphabets.  Mathematical symbols should be defined via the
   19.84 +  official rendering tables.
   19.85 +  </li>
   19.86 +
   19.87  </ul>
   19.88  
   19.89  
   19.90 -<h2>Limitations and workrounds (September 2011)</h2>
   19.91 +<h2>Limitations and workrounds (October 2011)</h2>
   19.92  
   19.93  <ul>
   19.94    <li>No way to start/stop prover or switch to a different logic.<br/>
   19.95 @@ -158,7 +193,7 @@
   19.96  </ul>
   19.97  
   19.98  
   19.99 -<h2>Known problems with Mac OS</h2>
  19.100 +<h2>Known problems with Mac OS X</h2>
  19.101  
  19.102  <ul>
  19.103  
  19.104 @@ -166,22 +201,21 @@
  19.105    e.g. between the editor and the Console plugin, which is a standard
  19.106    swing text box.  Similar for search boxes etc.</li>
  19.107  
  19.108 -<li>ToggleButton selected state is not rendered if window focus is
  19.109 -  lost, which is probably a genuine feature of the Apple
  19.110 -  look-and-feel.</li>
  19.111 -
  19.112 -<li>Font.createFont mangles the font family of non-regular fonts,
  19.113 -  e.g. bold.  IsabelleText font files need to be installed/updated
  19.114 -  manually.</li>
  19.115 +<li><tt>Font.createFont</tt> mangles the font family of non-regular
  19.116 +  fonts, e.g. bold.  IsabelleText font files need to be
  19.117 +  installed/updated manually if bold versions are desired.  Note that
  19.118 +  this has to be repeated whenever fonts shipped with Isabelle are
  19.119 +  updated!</li>
  19.120  
  19.121  <li>Missing glyphs are collected from other fonts (like Emacs,
  19.122 -  Firefox).  This is actually an advantage over the Oracle/Sun JVM on
  19.123 -  Windows or Linux, but probably also the deeper reason for the other
  19.124 -  oddities of Apple font management.</li>
  19.125 +  Firefox).  This is actually an advantage over the Oracle JVM on
  19.126 +  Windows or Linux, but also the deeper reason for other oddities of
  19.127 +  Apple font management.</li>
  19.128  
  19.129 -<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
  19.130 -  (not enabled by default) fails to handle the infinitesimal font size
  19.131 -  of "hidden" text (e.g.  used in Isabelle sub/superscripts).</li>
  19.132 +<li>The native font renderer
  19.133 +  of <tt>-Dapple.awt.graphics.UseQuartz=true</tt> (<em>not</em>
  19.134 +  enabled by default) fails to handle the infinitesimal font size of
  19.135 +  "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
  19.136  
  19.137  </ul>
  19.138  
  19.139 @@ -191,23 +225,10 @@
  19.140  <ul>
  19.141  
  19.142  <li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
  19.143 -  of the jEdit text area.  Always use official JRE 1.6.x from
  19.144 -  Sun/Oracle/Apple.</li>
  19.145 -
  19.146 -<li>jEdit on OpenJDK is generally not supported.</li>
  19.147 -
  19.148 -</ul>
  19.149 -
  19.150 +  of the jEdit text area.  Always use official JRE 1.6.x from Oracle
  19.151 +  or Apple.</li>
  19.152  
  19.153 -<h2>Known problems with Windows/Cygwin</h2>
  19.154 -
  19.155 -<ul>
  19.156 -
  19.157 -<li>Occasional session startup problems when loading a logic image
  19.158 -takes too long (cf. output in "Prover Session / Syslog" panel).</li>
  19.159 -
  19.160 -<li>Auxiliary files of a theory (<tt>uses</tt>) cannot be loaded due
  19.161 -to incompatible path notation inherited from MS-DOS.</li>
  19.162 +<li>jEdit 4.4.x on OpenJDK is generally not supported.</li>
  19.163  
  19.164  </ul>
  19.165  
  19.166 @@ -216,6 +237,8 @@
  19.167  
  19.168  <ul>
  19.169  
  19.170 +<li>Isabelle: BSD-style</li>
  19.171 +
  19.172  <li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
  19.173  
  19.174  <li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
    20.1 --- a/src/Tools/jEdit/src/html_panel.scala	Sun Oct 09 11:13:53 2011 +0200
    20.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Mon Oct 10 11:12:09 2011 +0200
    20.3 @@ -113,7 +113,7 @@
    20.4    /* internal messages */
    20.5  
    20.6    private case class Resize(font_family: String, font_size: Int)
    20.7 -  private case class Render_Document(text: String)
    20.8 +  private case class Render_Document(url: String, text: String)
    20.9    private case class Render(body: XML.Body)
   20.10    private case class Render_Sync(body: XML.Body)
   20.11    private case object Refresh
   20.12 @@ -151,9 +151,9 @@
   20.13  
   20.14      def refresh() { render(current_body) }
   20.15  
   20.16 -    def render_document(text: String)
   20.17 +    def render_document(url: String, text: String)
   20.18      {
   20.19 -      val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
   20.20 +      val doc = builder.parse(new InputSourceImpl(new StringReader(text), url))
   20.21        Swing_Thread.later { setDocument(doc, rcontext) }
   20.22      }
   20.23  
   20.24 @@ -183,7 +183,7 @@
   20.25        react {
   20.26          case Resize(font_family, font_size) => resize(font_family, font_size)
   20.27          case Refresh => refresh()
   20.28 -        case Render_Document(text) => render_document(text)
   20.29 +        case Render_Document(url, text) => render_document(url, text)
   20.30          case Render(body) => render(body)
   20.31          case Render_Sync(body) => render(body); reply(())
   20.32          case bad => System.err.println("main_actor: ignoring bad message " + bad)
   20.33 @@ -196,7 +196,7 @@
   20.34  
   20.35    def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   20.36    def refresh() { main_actor ! Refresh }
   20.37 -  def render_document(text: String) { main_actor ! Render_Document(text) }
   20.38 +  def render_document(url: String, text: String) { main_actor ! Render_Document(url, text) }
   20.39    def render(body: XML.Body) { main_actor ! Render(body) }
   20.40    def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
   20.41  }
    21.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Oct 09 11:13:53 2011 +0200
    21.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Oct 10 11:12:09 2011 +0200
    21.3 @@ -27,7 +27,10 @@
    21.4    /* main tabs */
    21.5  
    21.6    private val readme = new HTML_Panel("SansSerif", 14)
    21.7 -  readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html"))))
    21.8 +  private val readme_path = Path.explode("$JEDIT_HOME/README.html")
    21.9 +  readme.render_document(
   21.10 +    Isabelle_System.platform_file_url(readme_path),
   21.11 +    Isabelle_System.try_read(List(readme_path)))
   21.12  
   21.13    val status = new ListView(Nil: List[Document.Node.Name]) {
   21.14      listenTo(mouse.clicks)
    22.1 --- a/src/Tools/subtyping.ML	Sun Oct 09 11:13:53 2011 +0200
    22.2 +++ b/src/Tools/subtyping.ML	Mon Oct 10 11:12:09 2011 +0200
    22.3 @@ -628,7 +628,7 @@
    22.4                  NONE => raise COERCION_GEN_ERROR (err ++> quote (Syntax.string_of_typ ctxt T1) ^
    22.5                    " is not a subtype of " ^ quote (Syntax.string_of_typ ctxt T2))
    22.6                | SOME (co, _) => co)
    22.7 -      | ((Type (a, Ts)), (Type (b, Us))) =>
    22.8 +      | (T1 as Type (a, Ts), T2 as Type (b, Us)) =>
    22.9              if a <> b
   22.10              then
   22.11                (case Symreltab.lookup (coes_of ctxt) (a, b) of
   22.12 @@ -656,8 +656,11 @@
   22.13                    | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
   22.14                in
   22.15                  (case Symtab.lookup (tmaps_of ctxt) a of
   22.16 -                  NONE => raise COERCION_GEN_ERROR
   22.17 -                    (err ++> "No map function for " ^ quote a ^ " known")
   22.18 +                  NONE =>
   22.19 +                    if Type.could_unify (T1, T2)
   22.20 +                    then Abs (Name.uu, T1, Bound 0)
   22.21 +                    else raise COERCION_GEN_ERROR
   22.22 +                      (err ++> "No map function for " ^ quote a ^ " known")
   22.23                  | SOME tmap =>
   22.24                      let
   22.25                        val used_coes = map_filter sub_co ((snd tmap) ~~ (Ts ~~ Us));