slightly more standard data merge: Symtax.merge (K true) avoids equality on abstract type Pretty.T and gracefully accepts overriding, Symtab.join prefers first entry as usual;
(* Title: Pure/ProofGeneral/pgip.ML
Author: David Aspinall
Prover-side PGIP abstraction.
Not too closely tied to Isabelle, to help with reuse/porting.
*)
signature PGIP =
sig
include PGIPTYPES
include PGIPMARKUP
include PGIPINPUT
include PGIPOUTPUT
end
structure Pgip : PGIP =
struct
open PgipTypes
open PgipMarkup
open PgipInput
open PgipOutput
end