renamed isatool to isabelle_tool in programming interfaces;
authorwenzelm
Sat, 04 Oct 2008 14:29:43 +0200
changeset 28496 4cff10648928
parent 28495 c5f86d04743b
child 28497 40e1cc165b05
renamed isatool to isabelle_tool in programming interfaces;
src/Pure/General/file.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/present.ML
src/Pure/Tools/isabelle_system.scala
--- 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)
   }