--- a/Admin/Release/CHECKLIST Wed Feb 13 16:35:07 2013 +0100
+++ b/Admin/Release/CHECKLIST Wed Feb 13 17:41:27 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
--- a/lib/scripts/run-polyml Wed Feb 13 16:35:07 2013 +0100
+++ b/lib/scripts/run-polyml Wed Feb 13 17:41:27 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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/graphics_file.scala Wed Feb 13 17:41:27 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)
+}
+
--- a/src/Pure/build-jars Wed Feb 13 16:35:07 2013 +0100
+++ b/src/Pure/build-jars Wed Feb 13 17:41:27 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
--- a/src/Pure/proofterm.ML Wed Feb 13 16:35:07 2013 +0100
+++ b/src/Pure/proofterm.ML Wed Feb 13 17:41:27 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 =