src/Pure/Thy/present.ML
changeset 22580 d91b4dd651d6
parent 22123 15ddfafc04a9
child 22846 fb79144af9a3
--- a/src/Pure/Thy/present.ML	Wed Apr 04 00:11:08 2007 +0200
+++ b/src/Pure/Thy/present.ML	Wed Apr 04 00:11:10 2007 +0200
@@ -306,7 +306,8 @@
       val (doc_prefix1, documents) =
         if doc = "" then (NONE, [])
         else if not (File.exists document_path) then
-          (if verbose then std_error "Warning: missing document directory\n" else (); (NONE, []))
+          (if verbose then Output.std_error "Warning: missing document directory\n" else ();
+            (NONE, []))
         else (SOME (Path.append html_prefix document_path, html_prefix),
           read_versions doc_versions);
 
@@ -413,12 +414,12 @@
       File.copy (Path.explode "~~/lib/html/isabelle.css") html_prefix;
       List.app finish_html thys;
       List.app (uncurry File.write) files;
-      if verbose then std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
+      if verbose then Output.std_error ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
     else ();
 
     (case doc_prefix2 of NONE => () | SOME (cp, path) =>
      (prepare_sources cp path;
-      if verbose then std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
+      if verbose then Output.std_error ("Document sources at " ^ show_path path ^ "\n") else ()));
 
     (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
       documents |> List.app (fn (name, tags) =>
@@ -426,7 +427,7 @@
          val _ = prepare_sources true path;
          val doc_path = isatool_document true doc_format name tags path result_path;
        in
-         if verbose then std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
+         if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
        end));
 
     browser_info := empty_browser_info;