# HG changeset patch
# User wenzelm
# Date 1360769434 -3600
# Node ID 66d0298fc554afb54eac93656ae34e9bd4d1093f
# Parent  60e4b75fefe1cf090aa78697f40cae556eaaae01# Parent  18daa3380ff7699e8cb4079593c4645eb63563b9
merged

diff -r 60e4b75fefe1 -r 66d0298fc554 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Wed Feb 13 13:38:52 2013 +0100
+++ b/Admin/Release/CHECKLIST	Wed Feb 13 16:30:34 2013 +0100
@@ -59,7 +59,8 @@
 ===================
 
 - various .hg/hgrc files:
-  default = /home/isabelle-repository/repos/isabelle-release
+  default = http://bitbucket.org/isabelle_project/isabelle-release
+  default = ssh://hg@bitbucket.org/isabelle_project/isabelle-release
 
 - isatest@macbroy28:hg-isabelle/.hg/hgrc
 - isatest@macbroy28:devel-page/content/index.content
diff -r 60e4b75fefe1 -r 66d0298fc554 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Wed Feb 13 13:38:52 2013 +0100
+++ b/lib/scripts/run-polyml	Wed Feb 13 16:30:34 2013 +0100
@@ -49,7 +49,7 @@
   EXIT="fun exit rc : unit = Posix.Process.exit (Word8.fromInt rc);"
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle Fail msg => (TextIO.output (TextIO.stdErr, msg ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); Posix.Process.exit 0w1));"
   EXIT=""
 fi
 
@@ -57,7 +57,7 @@
   COMMIT='fun commit () = false;'
   MLEXIT=""
 else
-  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
+  COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   MLEXIT="commit();"
 fi
diff -r 60e4b75fefe1 -r 66d0298fc554 src/Pure/General/graphics_file.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/graphics_file.scala	Wed Feb 13 16:30:34 2013 +0100
@@ -0,0 +1,48 @@
+/*  Title:      Pure/General/graphics_file.scala
+    Author:     Makarius
+
+File system operations for Graphics2D output.
+*/
+
+package isabelle
+
+
+import java.awt.Graphics2D
+import java.io.{FileOutputStream, BufferedOutputStream, File => JFile}
+
+
+object Graphics_File
+{
+  /* PDF */
+
+  def write_pdf(file: JFile, paint: Graphics2D => Unit, width: Int, height: Int)
+  {
+    import com.lowagie.text.{Document, Rectangle}
+    import com.lowagie.text.pdf.PdfWriter
+
+    val out = new BufferedOutputStream(new FileOutputStream(file))
+    try {
+      val document = new Document()
+      try {
+        document.setPageSize(new Rectangle(width, height))
+        val writer = PdfWriter.getInstance(document, out)
+        document.open()
+
+        val cb = writer.getDirectContent()
+        val tp = cb.createTemplate(width, height)
+        val gfx = tp.createGraphics(width, height)
+
+        paint(gfx)
+        gfx.dispose
+
+        cb.addTemplate(tp, 1, 0, 0, 1, 0, 0)
+      }
+      finally { document.close() }
+    }
+    finally { out.close }
+  }
+
+  def write_pdf(path: Path, paint: Graphics2D => Unit, width: Int, height: Int): Unit =
+    write_pdf(path.file, paint, width, height)
+}
+
diff -r 60e4b75fefe1 -r 66d0298fc554 src/Pure/build-jars
--- a/src/Pure/build-jars	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/Pure/build-jars	Wed Feb 13 16:30:34 2013 +0100
@@ -16,6 +16,7 @@
   General/exn.scala
   General/file.scala
   General/graph.scala
+  General/graphics_file.scala
   General/linear_set.scala
   General/path.scala
   General/position.scala
diff -r 60e4b75fefe1 -r 66d0298fc554 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/Pure/proofterm.ML	Wed Feb 13 16:30:34 2013 +0100
@@ -1057,15 +1057,13 @@
 
 fun shrink_proof thy =
   let
-    val (typ, term) = Term_Sharing.init thy;
-
     fun shrink ls lev (prf as Abst (a, T, body)) =
           let val (b, is, ch, body') = shrink ls (lev+1) body
-          in (b, is, ch, if ch then Abst (a, Option.map typ T, body') else prf) end
+          in (b, is, ch, if ch then Abst (a, T, body') else prf) end
       | shrink ls lev (prf as AbsP (a, t, body)) =
           let val (b, is, ch, body') = shrink (lev::ls) lev body
           in (b orelse member (op =) is 0, map_filter (fn 0 => NONE | i => SOME (i-1)) is,
-            ch, if ch then AbsP (a, Option.map term t, body') else prf)
+            ch, if ch then AbsP (a, t, body') else prf)
           end
       | shrink ls lev prf =
           let val (is, ch, _, prf') = shrink' ls lev [] [] prf
@@ -1080,13 +1078,13 @@
       | shrink' ls lev ts prfs (prf as prf1 % t) =
           let val (is, ch, (ch', t')::ts', prf') = shrink' ls lev (t::ts) prfs prf1
           in (is, ch orelse ch', ts',
-              if ch orelse ch' then prf' % Option.map term t' else prf) end
+              if ch orelse ch' then prf' % t' else prf) end
       | shrink' ls lev ts prfs (prf as PBound i) =
           (if exists (fn SOME (Bound j) => lev-j <= nth ls i | _ => true) ts
              orelse has_duplicates (op =)
                (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
              orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
-      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (term t))
+      | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp t)
       | shrink' ls lev ts prfs (prf as MinProof) = ([], false, map (pair false) ts, prf)
       | shrink' ls lev ts prfs (prf as OfClass _) = ([], false, map (pair false) ts, prf)
       | shrink' ls lev ts prfs prf =