src/Pure/ProofGeneral/pgip_output.ML
changeset 21929 fb0cd849bc60
parent 21902 8e5e2571c716
child 21940 fbd068dd4d29
equal deleted inserted replaced
21928:266c2b1fbd6b 21929:fb0cd849bc60
   322 
   322 
   323 fun ready (Ready vs) = XML.Elem("ready",[],[])
   323 fun ready (Ready vs) = XML.Elem("ready",[],[])
   324 
   324 
   325 
   325 
   326 fun output pgipoutput = case pgipoutput of
   326 fun output pgipoutput = case pgipoutput of
   327  of Cleardisplay _          => cleardisplay pgipoutput
   327     Cleardisplay _          => cleardisplay pgipoutput
   328   | Normalresponse _        => normalresponse pgipoutput
   328   | Normalresponse _        => normalresponse pgipoutput
   329   | Errorresponse _         => errorresponse pgipoutput
   329   | Errorresponse _         => errorresponse pgipoutput
   330   | Informfileloaded _      => informfileloaded pgipoutput
   330   | Informfileloaded _      => informfileloaded pgipoutput
   331   | Informfileretracted _   => informfileretracted pgipoutput
   331   | Informfileretracted _   => informfileretracted pgipoutput
   332   | Proofstate _            => proofstate pgipoutput
   332   | Proofstate _            => proofstate pgipoutput