# HG changeset patch # User wenzelm # Date 1223123383 -7200 # Node ID 4cff10648928b8d4becaca339ff6bbd76fe89c80 # Parent c5f86d04743b3c0a75ea69e7672f432aa7a7a3c0 renamed isatool to isabelle_tool in programming interfaces; diff -r c5f86d04743b -r 4cff10648928 src/Pure/General/file.ML --- 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) diff -r c5f86d04743b -r 4cff10648928 src/Pure/Isar/isar_cmd.ML --- 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 *) diff -r c5f86d04743b -r 4cff10648928 src/Pure/Thy/present.ML --- 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; diff -r c5f86d04743b -r 4cff10648928 src/Pure/Tools/isabelle_system.scala --- 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) }