--- a/src/Pure/General/file.ML Sat Oct 04 14:29:42 2008 +0200
+++ b/src/Pure/General/file.ML Sat Oct 04 14:29:43 2008 +0200
@@ -13,7 +13,7 @@
val pwd: unit -> Path.T
val full_path: Path.T -> Path.T
val tmp_path: Path.T -> Path.T
- val isatool: string -> int
+ val isabelle_tool: string -> int
val system_command: string -> unit
eqtype ident
val rep_ident: ident -> string
@@ -66,7 +66,7 @@
(* system commands *)
-fun isatool cmd = system ("\"$ISATOOL\" " ^ cmd);
+fun isabelle_tool cmd = system ("\"$ISATOOL\" " ^ cmd);
fun system_command cmd =
if system cmd <> 0 then error ("System command failed: " ^ cmd)
--- a/src/Pure/Isar/isar_cmd.ML Sat Oct 04 14:29:42 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Sat Oct 04 14:29:43 2008 +0200
@@ -309,11 +309,11 @@
fun display_drafts files = Toplevel.imperative (fn () =>
let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
- in File.isatool ("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.isatool ("print -c " ^ outfile); () end);
+ in File.isabelle_tool ("print -c " ^ outfile); () end);
(* pretty_setmargin *)
--- a/src/Pure/Thy/present.ML Sat Oct 04 14:29:42 2008 +0200
+++ b/src/Pure/Thy/present.ML Sat Oct 04 14:29:43 2008 +0200
@@ -96,7 +96,7 @@
val _ = writeln "Displaying graph ...";
val path = File.tmp_path (Path.explode "tmp.graph");
val _ = write_graph gr path;
- val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");
+ val _ = File.isabelle_tool ("browser -c " ^ File.shell_path path ^ " &");
in () end;
@@ -321,9 +321,9 @@
end);
-(* isatool wrappers *)
+(* isabelle tool wrappers *)
-fun isatool_document verbose format name tags path result_path =
+fun isabelle_document verbose format name tags path result_path =
let
val s = "\"$ISATOOL\" document -c -o '" ^ format ^ "' \
\-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^
@@ -337,7 +337,7 @@
doc_path
end;
-fun isatool_browser graph =
+fun isabelle_browser graph =
let
val pdf_path = File.tmp_path graph_pdf_path;
val eps_path = File.tmp_path graph_eps_path;
@@ -345,7 +345,7 @@
val s = "browser -o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
in
write_graph graph gr_path;
- if File.isatool s <> 0 orelse not (File.exists eps_path) orelse not (File.exists pdf_path)
+ if File.isabelle_tool s <> 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
@@ -380,13 +380,13 @@
val sorted_graph = sorted_index graph;
val opt_graphs =
if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
- SOME (isatool_browser sorted_graph)
+ SOME (isabelle_browser sorted_graph)
else NONE;
fun prepare_sources cp path =
(File.mkdir path;
if cp then File.copy_dir document_path path else ();
- File.isatool ("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));
@@ -418,7 +418,7 @@
documents |> List.app (fn (name, tags) =>
let
val _ = prepare_sources true path;
- val doc_path = isatool_document true doc_format name tags path result_path;
+ val doc_path = isabelle_document true doc_format name tags path result_path;
in
if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
end));
@@ -514,8 +514,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.isatool ("latex -o sty " ^ File.shell_path root_path);
- val _ = File.isatool ("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)))
@@ -528,7 +528,7 @@
|> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
|> File.write (Path.append doc_path (tex_path name)));
val _ = write_tex_index tex_index doc_path;
- in isatool_document false doc_format documentN "" doc_path result_path end;
+ in isabelle_document false doc_format documentN "" doc_path result_path end;
end;
--- a/src/Pure/Tools/isabelle_system.scala Sat Oct 04 14:29:42 2008 +0200
+++ b/src/Pure/Tools/isabelle_system.scala Sat Oct 04 14:29:43 2008 +0200
@@ -91,7 +91,7 @@
/* Isabelle tools (non-interactive) */
- def isatool(args: String*) = {
+ def isabelle_tool(args: String*) = {
val proc =
try { exec2((List(getenv_strict("ISATOOL")) ++ args): _*) }
catch { case e: IOException => error(e.getMessage) }
@@ -105,13 +105,13 @@
/* named pipes */
def mk_fifo() = {
- val (result, rc) = isatool("mkfifo")
+ val (result, rc) = isabelle_tool("mkfifo")
if (rc == 0) result.trim
else error(result)
}
def rm_fifo(fifo: String) = {
- val (result, rc) = isatool("rmfifo", fifo)
+ val (result, rc) = isabelle_tool("rmfifo", fifo)
if (rc != 0) error(result)
}