# HG changeset patch
# User aspinall
# Date 1102714396 -3600
# Node ID ba28d103bada307d3f18ac80676ba7c54344578d
# Parent  50bbdabd7326eacb2d8405218ce9c2fdb34111f4
Support PGIP <whitespace>, <dostep>, <doitem> elements as input

diff -r 50bbdabd7326 -r ba28d103bada src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Fri Dec 10 22:25:31 2004 +0100
+++ b/src/Pure/proof_general.ML	Fri Dec 10 22:33:16 2004 +0100
@@ -1159,16 +1159,19 @@
 						(op =) 
 						(! print_mode, ["xsymbols", "symbols"])))
      (* properproofcmd: proper commands which belong in script *)
+     (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
      | "opengoal"       => isarscript data
      | "proofstep"      => isarscript data
      | "closegoal"      => isarscript data
      | "giveupgoal"     => isarscript data
      | "postponegoal"   => isarscript data
      | "comment"	=> isarscript data  (* NB: should be ignored, but process anyway *)
+     | "whitespace"	=> isarscript data  (* NB: should be ignored, but process anyway *)
      | "litcomment"     => isarscript data
      | "spuriouscmd"    => isarscript data
      | "badcmd"		=> isarscript data
      (* improperproofcmd: improper commands which *do not* belong in script *)
+     | "dostep"         => isarscript data
      | "undostep"       => isarcmd "undos_proof 1"
      | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
      | "forget"         => error "Not implemented" 
@@ -1183,6 +1186,7 @@
      | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext data))
      | "viewdoc"	=> isarcmd ("print_" ^ (xmltext data)) (* FIXME: isatool doc? *)
      (* properfilecmd: proper theory-level script commands *)
+     (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
      | "opentheory"     => isarscript data
      | "theoryitem"     => isarscript data
      | "closetheory"    => let 
@@ -1191,6 +1195,7 @@
 			       writeln ("Theory \""^thyname^"\" completed."))
 			   end
      (* improperfilecmd: theory-level commands not in script *)
+     | "doitem"         => isarscript data
      | "undoitem"       => isarcmd "ProofGeneral.undo"
      | "aborttheory"    => isarcmd ("init_toplevel")
      | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))