# HG changeset patch
# User wenzelm
# Date 1087716389 -7200
# Node ID 51f95648abadf649f03da9317a6cb15568095613
# Parent  18ee74d6bba1acc40f67be7508c20dd53a750c3f
tuned;

diff -r 18ee74d6bba1 -r 51f95648abad NEWS
--- 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 ***
diff -r 18ee74d6bba1 -r 51f95648abad lib/texinputs/draft.tex
--- 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{-}}%
diff -r 18ee74d6bba1 -r 51f95648abad src/Pure/General/pretty.ML
--- 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;
diff -r 18ee74d6bba1 -r 51f95648abad src/Pure/Thy/present.ML
--- 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))