system;
authorwenzelm
Wed Oct 13 19:41:35 1999 +0200 (1999-10-13)
changeset 7853a4acf1b4d5a8
parent 7852 d28dff7ac48d
child 7854 fe7b7e3c3ddc
system;
src/Pure/Thy/present.ML
src/Pure/Thy/thm_deps.ML
     1.1 --- a/src/Pure/Thy/present.ML	Wed Oct 13 19:41:18 1999 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Wed Oct 13 19:41:35 1999 +0200
     1.3 @@ -326,7 +326,7 @@
     1.4  
     1.5  fun isatool_document doc_format doc_prefix =
     1.6    let val cmd = "$ISATOOL document -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'"
     1.7 -  in writeln cmd; writeln (execute cmd) end;
     1.8 +  in writeln cmd; if system cmd <> 0 then error "Failed to build document" else () end;
     1.9  
    1.10  fun finish () = with_session ()
    1.11      (fn {name, html_prefix, doc_format, doc_prefix, graph_path, all_graph_path, path, ...} =>
     2.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Oct 13 19:41:18 1999 +0200
     2.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Oct 13 19:41:35 1999 +0200
     2.3 @@ -75,7 +75,7 @@
     2.4        map (#der o rep_thm) thms))));
     2.5      val path = File.tmp_path (Path.unpack "theorems.graph");
     2.6      val _ = put_graph gra path;
     2.7 -    val _ = execute ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
     2.8 +    val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
     2.9    in () end;
    2.10  
    2.11  end;