# HG changeset patch
# User wenzelm
# Date 1246116908 -7200
# Node ID 2c0ab4485f488432c1f4acd87352d457e95c3c84
# Parent  f698f76a371336a50dc8ec476449d70757184015
tune File.isabelle_tool signature;

diff -r f698f76a3713 -r 2c0ab4485f48 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Jun 27 17:34:48 2009 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Jun 27 17:35:08 2009 +0200
@@ -306,11 +306,11 @@
 
 fun display_drafts files = Toplevel.imperative (fn () =>
   let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
-  in File.isabelle_tool ("display -c " ^ outfile ^ " &"); () end);
+  in File.isabelle_tool "display" ("-c " ^ outfile ^ " &"); () end);
 
 fun print_drafts files = Toplevel.imperative (fn () =>
   let val outfile = File.shell_path (Present.drafts "ps" files)
-  in File.isabelle_tool ("print -c " ^ outfile); () end);
+  in File.isabelle_tool "print" ("-c " ^ outfile); () end);
 
 
 (* pretty_setmargin *)
diff -r f698f76a3713 -r 2c0ab4485f48 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Jun 27 17:34:48 2009 +0200
+++ b/src/Pure/Thy/present.ML	Sat Jun 27 17:35:08 2009 +0200
@@ -95,7 +95,7 @@
     val _ = writeln "Displaying graph ...";
     val path = File.tmp_path (Path.explode "tmp.graph");
     val _ = write_graph gr path;
-    val _ = File.isabelle_tool ("browser -c " ^ File.shell_path path ^ " &");
+    val _ = File.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
   in () end;
 
 
@@ -341,10 +341,11 @@
     val pdf_path = File.tmp_path graph_pdf_path;
     val eps_path = File.tmp_path graph_eps_path;
     val gr_path = File.tmp_path graph_path;
-    val s = "browser -o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
+    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
   in
     write_graph graph gr_path;
-    if File.isabelle_tool s <> 0 orelse not (File.exists eps_path) orelse not (File.exists pdf_path)
+    if File.isabelle_tool "browser" args <> 0 orelse
+      not (File.exists eps_path) orelse not (File.exists pdf_path)
     then error "Failed to prepare dependency graph"
     else
       let val pdf = File.read pdf_path and eps = File.read eps_path
@@ -385,7 +386,8 @@
     fun prepare_sources cp path =
      (File.mkdir path;
       if cp then File.copy_dir document_path path else ();
-      File.isabelle_tool ("latex -o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
+      File.isabelle_tool "latex"
+        ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
       (case opt_graphs of NONE => () | SOME (pdf, eps) =>
         (File.write (Path.append path graph_pdf_path) pdf;
           File.write (Path.append path graph_eps_path) eps));
@@ -513,8 +515,8 @@
     val _ = File.mkdir doc_path;
     val root_path = Path.append doc_path (Path.basic "root.tex");
     val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
-    val _ = File.isabelle_tool ("latex -o sty " ^ File.shell_path root_path);
-    val _ = File.isabelle_tool ("latex -o syms " ^ File.shell_path root_path);
+    val _ = File.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
+    val _ = File.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
 
     fun known name =
       let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))