--- a/NEWS Fri Jun 18 20:10:52 2004 +0200
+++ b/NEWS Sun Jun 20 09:26:29 2004 +0200
@@ -75,7 +75,8 @@
bypassing the standard channels (writeln etc.), or in token
translations to produce properly formatted results; Output.raw is
required when capturing already output material that will eventually
- be presented to the user a second time.
+ be presented to the user a second time. For the default print mode,
+ both Output.output and Output.raw have no effect.
*** HOL ***
--- a/lib/texinputs/draft.tex Fri Jun 18 20:10:52 2004 +0200
+++ b/lib/texinputs/draft.tex Sun Jun 20 09:26:29 2004 +0200
@@ -6,16 +6,13 @@
%%
\documentclass[10pt,a4paper]{article}
-\usepackage{isabelle,isabellesym}
+\usepackage{isabelle,isabellesym,pdfsetup}
-%packages for unusual symbols -- selection needs to conform to
-%result of 'isatool latex -o syms'
+%packages for unusual symbols according to 'isatool latex -o syms'
\usepackage[latin1]{inputenc}
\usepackage{amssymb}
\usepackage{textcomp}
-\usepackage{pdfsetup}
-
\pagestyle{myheadings}
\renewcommand{\isamarkupheader}[1]%
{{\def\isacharunderscore{\mbox{-}}%
--- a/src/Pure/General/pretty.ML Fri Jun 18 20:10:52 2004 +0200
+++ b/src/Pure/General/pretty.ML Sun Jun 20 09:26:29 2004 +0200
@@ -54,8 +54,7 @@
val setmargin: int -> unit
val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
type pp
- val pp: (term -> T) -> (typ -> T) -> (sort -> T) ->
- (class list -> T) -> (arity -> T) -> pp
+ val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
val pp_undef: pp
val term: pp -> term -> T
val typ: pp -> typ -> T
@@ -279,7 +278,7 @@
datatype pp =
PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
-fun pp f1 f2 f3 f4 f5 = PP (f1, f2, f3, f4, f5);
+val pp = PP;
fun pp_fun f (PP x) = f x;
@@ -297,6 +296,6 @@
fun undef kind _ = str ("*** UNABLE TO PRINT " ^ kind ^ " ***");
val pp_undef =
- pp (undef "term") (undef "typ") (undef "sort") (undef "classrel") (undef "arity");
+ pp (undef "term", undef "typ", undef "sort", undef "classrel", undef "arity");
end;
--- a/src/Pure/Thy/present.ML Fri Jun 18 20:10:52 2004 +0200
+++ b/src/Pure/Thy/present.ML Sun Jun 20 09:26:29 2004 +0200
@@ -327,11 +327,12 @@
let
val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^
File.quote_sysify_path path ^ " 2>&1" ^ (if verbose then "" else " >/dev/null");
+ val doc_path = Path.ext doc_format path;
in
if verbose then writeln s else ();
system s;
- if File.exists (Path.ext doc_format path) then ()
- else error "Failed to build document"
+ if File.exists doc_path then ()
+ else error ("No document: " ^ quote (Path.pack (Path.expand doc_path)))
end;
fun isatool_browser graph =
@@ -499,7 +500,8 @@
fun prep_draft (tex_index, path) =
let
val base = Path.base path;
- val name = Path.pack (#1 (Path.split_ext base));
+ val name =
+ (case Path.pack (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
in
if File.exists path then
(Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))