structure Systeml :> Systeml = struct

(* This is the WINDOWS implementation of the Systeml functionality.
   It is the very first thing compiled by the HOL build process so it
   absolutely can not depend on any other HOL source code. *)

structure Process = OS.Process
structure Path = OS.Path
structure FileSys = OS.FileSys

fun dquote s = concat ["\"", s, "\""]

fun concat_wspaces munge acc strl =
    case strl of
      [] => concat (List.rev acc)
    | [x] => concat (List.rev (munge x :: acc))
    | (x::xs) => concat_wspaces munge (" " :: munge x :: acc) xs

fun systeml l = let
  val command = "call "^concat_wspaces dquote [] l
in
  Process.system command
end

val protect = dquote

(* the _ps suffix stands for 'protected string', as opposed to the 'l'
   of systeml, which stands for 'list' of strings (all of which are
   presumed unprotected).  The problem is that on Windows, if you pass
   system a (protected) string such as
      "c:/program files/bar/baz" "arg1"
   then it has a fit.  It seems the only way of getting it to play nicely
   is to prefix the commandline with "call". *)
fun system_ps s = Process.system ("call " ^ s)

fun xable_string s = s^".exe"
fun mk_xable file =   (* returns the name of the executable *)
    let val exe = file^".exe"
        val _ = FileSys.remove exe handle _ => ()
    in
      FileSys.rename{old=file, new=exe};
      exe
    end

fun normPath s = Path.toString(Path.fromString s)

fun fullPath slist =
    normPath (List.foldl (fn (p1,p2) => Path.concat(p2,p1))
                         (hd slist) (tl slist))

val HOLDIR =
val MOSMLDIR =
val OS =
val DEPDIR =
val GNUMAKE =
val DYNLIB =
val version =
val release =
val DOT_PATH =
val POLY = ""
val POLYC = ""
val DEFAULT_STATE = fullPath [HOLDIR, "bin", "hol.state"]
val POLY_VERSION = PolyML.Compiler.compilerVersionNumber

val isUnix = false
val pointer_eq = PolyML.pointerEq

val build_log_dir = fullPath [HOLDIR, "tools", "build-logs"]
val build_log_file = fullPath [build_log_dir, "current-build-log"]
val make_log_file = "current-make-log"
val build_after_reloc_envvar = "HOL_REBUILD_HEAPS_ONLY"

local
  fun fopen file = (FileSys.remove file handle _ => (); TextIO.openOut file)
  fun munge s = String.translate (fn #"/" => "\\" | c => str c) s
  fun q s = "\""^munge s^"\""
in
fun emit_hol_script target qend =
 let val ostrm = fopen(target^".bat")
     fun output s = TextIO.output(ostrm, s)
     val sigobj = q (fullPath [HOLDIR, "sigobj"])
     val std_prelude = q (fullPath [HOLDIR, "std.prelude"])
     val mosml = q (fullPath [MOSMLDIR, "mosml"])
 in
    output "@echo off\n";
    output "rem The bare HOL script\n";
    output "rem (automatically generated by HOL configuration)\n\n";
    output (String.concat["call ", mosml, " -P full -I ", sigobj, " ",
                          std_prelude, " %* ", q qend, "\n"]);
    TextIO.closeOut ostrm;
    target
 end


fun emit_hol_unquote_script target qend =
 let val ostrm = fopen(target^".bat")
     fun output s = TextIO.output(ostrm, s)
     val qfilter = q (fullPath [HOLDIR, "bin", "unquote"])
     val sigobj = q (fullPath [HOLDIR, "sigobj"])
     val std_prelude = q (fullPath [HOLDIR, "std.prelude"])
     val mosml = q (fullPath [MOSMLDIR, "mosml"])
     val qinit = q (fullPath [HOLDIR, "tools", "unquote-init.sml"])
 in
    output "@echo off\n";
    output "rem The HOL script (with quote preprocessing)\n";
    output "rem (automatically generated by HOL configuration)\n\n";
    output  (String.concat ["call ", qfilter, " | ", mosml,
                          " -P full -I ", sigobj, " ",
                            std_prelude, " ", qinit, " %* ",
                            q qend, "\n"]);
    TextIO.closeOut ostrm;
    target
 end
end (* local *)


end; (* struct *)