# HG changeset patch
# User aspinall
# Date 1092871217 -7200
# Node ID e1ed51e0ec0f948d7c8aa642f9fb91371c92174b
# Parent  eab7de0d0a3180bca67c87d57d4efa113ff0c3b5
Add systemcmd.

diff -r eab7de0d0a31 -r e1ed51e0ec0f src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Thu Aug 19 00:47:15 2004 +0200
+++ b/src/Pure/proof_general.ML	Thu Aug 19 01:20:17 2004 +0200
@@ -1127,6 +1127,7 @@
 			      | None => raise PGIP ("closefile when no file is open!"))
      | "abortfile"      => (currently_open_file := None) (* perhaps error for no file open *)
      | "changecwd"      => ThyLoad.add_path (xmlattr attrs dirname_attr)
+     | "systemcmd"	=> isarscript data
      (* unofficial command for debugging *)
      | "quitpgip" => raise PGIP_QUIT  
      | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))