Allow user to configure location of dot tool for theory graph building.

The default is /usr/bin/dot, because that’s where it is on my Linux machine.  If you need it to be somewhere else, create a config-override or poly-includes.ML file, depending on which ML you’re using.

help/src-sml/DOT

@@ -35,7 +35,7 @@ val HTML_DIR   = Path.toString(Path.fromString(Path.concat
 val SIGOBJ_DIR = Path.toString(Path.fromString(Path.concat
                     (Globals.HOLDIR,"sigobj")));
 
-val DOTPATH = "/usr/local/bin/dot"
+val DOTPATH = Systeml.DOT_PATH
 
 (*---------------------------------------------------------------------------
      Extract dot-friendly digraph from HOL theory graph.
@@ -227,4 +227,3 @@ val _ = print " done\n";
 
 
 gen_map_file DOTPATH ancs (Path.concat(HTML_DIR, "theories"));
-

tools-poly/Holmake/unix-systeml.sml

@@ -99,6 +99,7 @@ val DYNLIB = ""
 val version = ""
 val ML_SYSNAME = ""
 val release = ""
+val DOT_PATH = ""
 
 val isUnix = true
 

tools-poly/Holmake/winNT-systeml.sml

@@ -56,6 +56,7 @@ val GNUMAKE =
 val DYNLIB =
 val version =
 val release =
+val DOT_PATH =
 
 val isUnix = false
 
@@ -108,5 +109,3 @@ end (* local *)
 
 
 end; (* struct *)
-
-

tools-poly/configure.sml

@@ -232,7 +232,8 @@ in
    "val DYNLIB ="   --> ("val DYNLIB = "^Bool.toString dynlib_available^"\n"),
    "val version ="  --> ("val version = "^Int.toString version_number^"\n"),
    "val ML_SYSNAME =" --> "val ML_SYSNAME = \"poly\"\n",
-   "val release ="  --> ("val release = "^quote release_string^"\n")];
+   "val release ="  --> ("val release = "^quote release_string^"\n"),
+   "val DOT_PATH =" --> ("val DOT_PATH = "^quote DOT_PATH^"\n")];
   use destfile
 end;
 

tools-poly/smart-configure.sml

@@ -212,6 +212,8 @@ val dynlib_available = false;
 
 print "\n";
 
+val DOT_PATH = "/usr/bin/dot"
+
 fun verdict (prompt, value) =
     if value = "" then
       (print ("\n*** No value for "^prompt^
@@ -226,6 +228,7 @@ verdict ("OS", OS);
 verdict ("poly", poly);
 verdict ("polymllibdir", polymllibdir);
 verdict ("holdir", holdir);
+verdict ("DOT_PATH", DOT_PATH);
 
 print "\nConfiguration will begin with above values.  If they are wrong\n";
 print "press Control-C.\n\n";

tools/Holmake/Systeml.sig

@@ -29,6 +29,7 @@ sig
   val GNUMAKE : string
   val DYNLIB : bool
   val ML_SYSNAME : string
+  val DOT_PATH : string
 
   val isUnix : bool
 

tools/Holmake/unix-systeml.sml

@@ -102,6 +102,7 @@ val DYNLIB = ""
 val version = ""
 val ML_SYSNAME = ""
 val release = ""
+val DOT_PATH = ""
 
 val isUnix = true
 

tools/Holmake/winNT-systeml.sml

@@ -94,6 +94,7 @@ val DYNLIB = ""
 val version = ""
 val ML_SYSNAME = ""
 val release = ""
+val DOT_PATH = ""
 
 val isUnix = false
 

tools/configure-mosml.sml

@@ -179,6 +179,8 @@ val dynlib_available = (load "Dynlib"; true) handle _ => false;
 
 print "\n";
 
+val DOT_PATH = "/usr/bin/dot"
+
 val _ = let
   val override = Path.concat(holdir, "config-override")
 in
@@ -199,6 +201,7 @@ verdict ("OS", OS);
 verdict ("mosmldir", mosmldir);
 verdict ("holdir", holdir);
 verdict ("dynlib_available", Bool.toString dynlib_available);
+verdict ("DOT_PATH", DOT_PATH);
 
 val _ = let
   val mosml' = if OS = "winNT" then "mosmlc.exe" else "mosmlc"

tools/configure.sml

@@ -185,7 +185,9 @@ in
    "val DYNLIB ="   --> ("val DYNLIB = "^Bool.toString dynlib_available^"\n"),
    "val version ="  --> ("val version = "^Int.toString version_number^"\n"),
    "val ML_SYSNAME =" --> "val ML_SYSNAME = \"mosml\"\n",
-   "val release ="  --> ("val release = "^quote release_string^"\n")];
+   "val release ="  --> ("val release = "^quote release_string^"\n"),
+   "val DOT_PATH =" --> ("val DOT_PATH = "^quote DOT_PATH^"\n")
+  ];
   use destfile
 end;