1.1 --- a/NEWS	Fri Jun 18 20:10:52 2004 +0200
     1.2 +++ b/NEWS	Sun Jun 20 09:26:29 2004 +0200
     1.3 @@ -75,7 +75,8 @@
     1.4    bypassing the standard channels (writeln etc.), or in token
     1.5    translations to produce properly formatted results; Output.raw is
     1.6    required when capturing already output material that will eventually
     1.7 -  be presented to the user a second time.
     1.8 +  be presented to the user a second time.  For the default print mode,
     1.9 +  both Output.output and Output.raw have no effect.
    1.10  
    1.11  
    1.12  *** HOL ***

     2.1 --- a/lib/texinputs/draft.tex	Fri Jun 18 20:10:52 2004 +0200
     2.2 +++ b/lib/texinputs/draft.tex	Sun Jun 20 09:26:29 2004 +0200
     2.3 @@ -6,16 +6,13 @@
     2.4  %%
     2.5  
     2.6  \documentclass[10pt,a4paper]{article}
     2.7 -\usepackage{isabelle,isabellesym}
     2.8 +\usepackage{isabelle,isabellesym,pdfsetup}
     2.9  
    2.10 -%packages for unusual symbols -- selection needs to conform to
    2.11 -%result of 'isatool latex -o syms'
    2.12 +%packages for unusual symbols according to 'isatool latex -o syms'
    2.13  \usepackage[latin1]{inputenc}
    2.14  \usepackage{amssymb}
    2.15  \usepackage{textcomp}
    2.16  
    2.17 -\usepackage{pdfsetup}
    2.18 -
    2.19  \pagestyle{myheadings}
    2.20  \renewcommand{\isamarkupheader}[1]%
    2.21  {{\def\isacharunderscore{\mbox{-}}%

     3.1 --- a/src/Pure/General/pretty.ML	Fri Jun 18 20:10:52 2004 +0200
     3.2 +++ b/src/Pure/General/pretty.ML	Sun Jun 20 09:26:29 2004 +0200
     3.3 @@ -54,8 +54,7 @@
     3.4    val setmargin: int -> unit
     3.5    val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
     3.6    type pp
     3.7 -  val pp: (term -> T) -> (typ -> T) -> (sort -> T) ->
     3.8 -    (class list -> T) -> (arity -> T)  -> pp
     3.9 +  val pp: (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T) -> pp
    3.10    val pp_undef: pp
    3.11    val term: pp -> term -> T
    3.12    val typ: pp -> typ -> T
    3.13 @@ -279,7 +278,7 @@
    3.14  datatype pp =
    3.15    PP of (term -> T) * (typ -> T) * (sort -> T) * (class list -> T) * (arity -> T);
    3.16  
    3.17 -fun pp f1 f2 f3 f4 f5 = PP (f1, f2, f3, f4, f5);
    3.18 +val pp = PP;
    3.19  
    3.20  fun pp_fun f (PP x) = f x;
    3.21  
    3.22 @@ -297,6 +296,6 @@
    3.23  
    3.24  fun undef kind _ = str ("*** UNABLE TO PRINT " ^ kind ^ " ***");
    3.25  val pp_undef =
    3.26 -  pp (undef "term") (undef "typ") (undef "sort") (undef "classrel") (undef "arity");
    3.27 +  pp (undef "term", undef "typ", undef "sort", undef "classrel", undef "arity");
    3.28  
    3.29  end;

     4.1 --- a/src/Pure/Thy/present.ML	Fri Jun 18 20:10:52 2004 +0200
     4.2 +++ b/src/Pure/Thy/present.ML	Sun Jun 20 09:26:29 2004 +0200
     4.3 @@ -327,11 +327,12 @@
     4.4    let
     4.5      val s = "\"$ISATOOL\" document -c -o '" ^ doc_format ^ "' " ^
     4.6        File.quote_sysify_path path ^ " 2>&1" ^ (if verbose then "" else " >/dev/null");
     4.7 +    val doc_path = Path.ext doc_format path;
     4.8    in
     4.9      if verbose then writeln s else ();
    4.10      system s;
    4.11 -    if File.exists (Path.ext doc_format path) then ()
    4.12 -    else error "Failed to build document"
    4.13 +    if File.exists doc_path then ()
    4.14 +    else error ("No document: " ^ quote (Path.pack (Path.expand doc_path)))
    4.15    end;
    4.16  
    4.17  fun isatool_browser graph =
    4.18 @@ -499,7 +500,8 @@
    4.19      fun prep_draft (tex_index, path) =
    4.20        let
    4.21          val base = Path.base path;
    4.22 -        val name = Path.pack (#1 (Path.split_ext base));
    4.23 +        val name =
    4.24 +          (case Path.pack (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
    4.25        in
    4.26          if File.exists path then
    4.27            (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))