src/Pure/Thy/present.ML
changeset 31819 2c0ab4485f48
parent 29606 fedb8be05f24
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/Thy/present.ML	Sat Jun 27 17:34:48 2009 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Sat Jun 27 17:35:08 2009 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4      val _ = writeln "Displaying graph ...";
     1.5      val path = File.tmp_path (Path.explode "tmp.graph");
     1.6      val _ = write_graph gr path;
     1.7 -    val _ = File.isabelle_tool ("browser -c " ^ File.shell_path path ^ " &");
     1.8 +    val _ = File.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
     1.9    in () end;
    1.10  
    1.11  
    1.12 @@ -341,10 +341,11 @@
    1.13      val pdf_path = File.tmp_path graph_pdf_path;
    1.14      val eps_path = File.tmp_path graph_eps_path;
    1.15      val gr_path = File.tmp_path graph_path;
    1.16 -    val s = "browser -o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
    1.17 +    val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
    1.18    in
    1.19      write_graph graph gr_path;
    1.20 -    if File.isabelle_tool s <> 0 orelse not (File.exists eps_path) orelse not (File.exists pdf_path)
    1.21 +    if File.isabelle_tool "browser" args <> 0 orelse
    1.22 +      not (File.exists eps_path) orelse not (File.exists pdf_path)
    1.23      then error "Failed to prepare dependency graph"
    1.24      else
    1.25        let val pdf = File.read pdf_path and eps = File.read eps_path
    1.26 @@ -385,7 +386,8 @@
    1.27      fun prepare_sources cp path =
    1.28       (File.mkdir path;
    1.29        if cp then File.copy_dir document_path path else ();
    1.30 -      File.isabelle_tool ("latex -o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
    1.31 +      File.isabelle_tool "latex"
    1.32 +        ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
    1.33        (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    1.34          (File.write (Path.append path graph_pdf_path) pdf;
    1.35            File.write (Path.append path graph_eps_path) eps));
    1.36 @@ -513,8 +515,8 @@
    1.37      val _ = File.mkdir doc_path;
    1.38      val root_path = Path.append doc_path (Path.basic "root.tex");
    1.39      val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
    1.40 -    val _ = File.isabelle_tool ("latex -o sty " ^ File.shell_path root_path);
    1.41 -    val _ = File.isabelle_tool ("latex -o syms " ^ File.shell_path root_path);
    1.42 +    val _ = File.isabelle_tool "latex" ("-o sty " ^ File.shell_path root_path);
    1.43 +    val _ = File.isabelle_tool "latex" ("-o syms " ^ File.shell_path root_path);
    1.44  
    1.45      fun known name =
    1.46        let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))