renamed isatool to isabelle_tool in programming interfaces;
authorwenzelm
Sat Oct 04 14:29:43 2008 +0200 (2008-10-04 ago)
changeset 284964cff10648928
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
     1.1 --- a/src/Pure/General/file.ML	Sat Oct 04 14:29:42 2008 +0200
     1.2 +++ b/src/Pure/General/file.ML	Sat Oct 04 14:29:43 2008 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    val pwd: unit -> Path.T
     1.5    val full_path: Path.T -> Path.T
     1.6    val tmp_path: Path.T -> Path.T
     1.7 -  val isatool: string -> int
     1.8 +  val isabelle_tool: string -> int
     1.9    val system_command: string -> unit
    1.10    eqtype ident
    1.11    val rep_ident: ident -> string
    1.12 @@ -66,7 +66,7 @@
    1.13  
    1.14  (* system commands *)
    1.15  
    1.16 -fun isatool cmd = system ("\"$ISATOOL\" " ^ cmd);
    1.17 +fun isabelle_tool cmd = system ("\"$ISATOOL\" " ^ cmd);
    1.18  
    1.19  fun system_command cmd =
    1.20    if system cmd <> 0 then error ("System command failed: " ^ cmd)
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Oct 04 14:29:42 2008 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Oct 04 14:29:43 2008 +0200
     2.3 @@ -309,11 +309,11 @@
     2.4  
     2.5  fun display_drafts files = Toplevel.imperative (fn () =>
     2.6    let val outfile = File.shell_path (Present.drafts (getenv "ISABELLE_DOC_FORMAT") files)
     2.7 -  in File.isatool ("display -c " ^ outfile ^ " &"); () end);
     2.8 +  in File.isabelle_tool ("display -c " ^ outfile ^ " &"); () end);
     2.9  
    2.10  fun print_drafts files = Toplevel.imperative (fn () =>
    2.11    let val outfile = File.shell_path (Present.drafts "ps" files)
    2.12 -  in File.isatool ("print -c " ^ outfile); () end);
    2.13 +  in File.isabelle_tool ("print -c " ^ outfile); () end);
    2.14  
    2.15  
    2.16  (* pretty_setmargin *)
     3.1 --- a/src/Pure/Thy/present.ML	Sat Oct 04 14:29:42 2008 +0200
     3.2 +++ b/src/Pure/Thy/present.ML	Sat Oct 04 14:29:43 2008 +0200
     3.3 @@ -96,7 +96,7 @@
     3.4      val _ = writeln "Displaying graph ...";
     3.5      val path = File.tmp_path (Path.explode "tmp.graph");
     3.6      val _ = write_graph gr path;
     3.7 -    val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");
     3.8 +    val _ = File.isabelle_tool ("browser -c " ^ File.shell_path path ^ " &");
     3.9    in () end;
    3.10  
    3.11  
    3.12 @@ -321,9 +321,9 @@
    3.13      end);
    3.14  
    3.15  
    3.16 -(* isatool wrappers *)
    3.17 +(* isabelle tool wrappers *)
    3.18  
    3.19 -fun isatool_document verbose format name tags path result_path =
    3.20 +fun isabelle_document verbose format name tags path result_path =
    3.21    let
    3.22      val s = "\"$ISATOOL\" document -c -o '" ^ format ^ "' \
    3.23        \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.shell_path path ^
    3.24 @@ -337,7 +337,7 @@
    3.25      doc_path
    3.26    end;
    3.27  
    3.28 -fun isatool_browser graph =
    3.29 +fun isabelle_browser graph =
    3.30    let
    3.31      val pdf_path = File.tmp_path graph_pdf_path;
    3.32      val eps_path = File.tmp_path graph_eps_path;
    3.33 @@ -345,7 +345,7 @@
    3.34      val s = "browser -o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path gr_path;
    3.35    in
    3.36      write_graph graph gr_path;
    3.37 -    if File.isatool s <> 0 orelse not (File.exists eps_path) orelse not (File.exists pdf_path)
    3.38 +    if File.isabelle_tool s <> 0 orelse not (File.exists eps_path) orelse not (File.exists pdf_path)
    3.39      then error "Failed to prepare dependency graph"
    3.40      else
    3.41        let val pdf = File.read pdf_path and eps = File.read eps_path
    3.42 @@ -380,13 +380,13 @@
    3.43      val sorted_graph = sorted_index graph;
    3.44      val opt_graphs =
    3.45        if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
    3.46 -        SOME (isatool_browser sorted_graph)
    3.47 +        SOME (isabelle_browser sorted_graph)
    3.48        else NONE;
    3.49  
    3.50      fun prepare_sources cp path =
    3.51       (File.mkdir path;
    3.52        if cp then File.copy_dir document_path path else ();
    3.53 -      File.isatool ("latex -o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
    3.54 +      File.isabelle_tool ("latex -o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
    3.55        (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    3.56          (File.write (Path.append path graph_pdf_path) pdf;
    3.57            File.write (Path.append path graph_eps_path) eps));
    3.58 @@ -418,7 +418,7 @@
    3.59        documents |> List.app (fn (name, tags) =>
    3.60         let
    3.61           val _ = prepare_sources true path;
    3.62 -         val doc_path = isatool_document true doc_format name tags path result_path;
    3.63 +         val doc_path = isabelle_document true doc_format name tags path result_path;
    3.64         in
    3.65           if verbose then Output.std_error ("Document at " ^ show_path doc_path ^ "\n") else ()
    3.66         end));
    3.67 @@ -514,8 +514,8 @@
    3.68      val _ = File.mkdir doc_path;
    3.69      val root_path = Path.append doc_path (Path.basic "root.tex");
    3.70      val _ = File.copy (Path.explode "~~/lib/texinputs/draft.tex") root_path;
    3.71 -    val _ = File.isatool ("latex -o sty " ^ File.shell_path root_path);
    3.72 -    val _ = File.isatool ("latex -o syms " ^ File.shell_path root_path);
    3.73 +    val _ = File.isabelle_tool ("latex -o sty " ^ File.shell_path root_path);
    3.74 +    val _ = File.isabelle_tool ("latex -o syms " ^ File.shell_path root_path);
    3.75  
    3.76      fun known name =
    3.77        let val ss = split_lines (File.read (Path.append doc_path (Path.basic name)))
    3.78 @@ -528,7 +528,7 @@
    3.79        |> Latex.symbol_source (known_syms, known_ctrls) (Path.implode base)
    3.80        |> File.write (Path.append doc_path (tex_path name)));
    3.81      val _ = write_tex_index tex_index doc_path;
    3.82 -  in isatool_document false doc_format documentN "" doc_path result_path end;
    3.83 +  in isabelle_document false doc_format documentN "" doc_path result_path end;
    3.84  
    3.85  
    3.86  end;
     4.1 --- a/src/Pure/Tools/isabelle_system.scala	Sat Oct 04 14:29:42 2008 +0200
     4.2 +++ b/src/Pure/Tools/isabelle_system.scala	Sat Oct 04 14:29:43 2008 +0200
     4.3 @@ -91,7 +91,7 @@
     4.4  
     4.5    /* Isabelle tools (non-interactive) */
     4.6  
     4.7 -  def isatool(args: String*) = {
     4.8 +  def isabelle_tool(args: String*) = {
     4.9      val proc =
    4.10        try { exec2((List(getenv_strict("ISATOOL")) ++ args): _*) }
    4.11        catch { case e: IOException => error(e.getMessage) }
    4.12 @@ -105,13 +105,13 @@
    4.13    /* named pipes */
    4.14  
    4.15    def mk_fifo() = {
    4.16 -    val (result, rc) = isatool("mkfifo")
    4.17 +    val (result, rc) = isabelle_tool("mkfifo")
    4.18      if (rc == 0) result.trim
    4.19      else error(result)
    4.20    }
    4.21  
    4.22    def rm_fifo(fifo: String) = {
    4.23 -    val (result, rc) = isatool("rmfifo", fifo)
    4.24 +    val (result, rc) = isabelle_tool("rmfifo", fifo)
    4.25      if (rc != 0) error(result)
    4.26    }
    4.27