# HG changeset patch # User wenzelm # Date 1184192138 -7200 # Node ID ec6f7a398625f8291d822fa3002218c926fb61bb # Parent 20f58293fc5e95a0db8de8ecf198143e64a2e77e added skeleton for print_mode setup; removed unused stuff; diff -r 20f58293fc5e -r ec6f7a398625 src/Pure/ProofGeneral/pgml_isabelle.ML --- a/src/Pure/ProofGeneral/pgml_isabelle.ML Thu Jul 12 00:15:37 2007 +0200 +++ b/src/Pure/ProofGeneral/pgml_isabelle.ML Thu Jul 12 00:15:38 2007 +0200 @@ -1,28 +1,23 @@ -(* Title: Pure/ProofGeneral/pgip_types.ML +(* Title: Pure/ProofGeneral/pgml_isabelle.ML ID: $Id$ Author: David Aspinall -PGIP abstraction: marshalling between PGML and Isabelle types +PGML print mode for common Isabelle markup. *) signature PGML_ISABELLE = sig -(* val pgml_of_prettyT : Pretty.T -> Pgml.pgmlterm *) + val pgml_mode: ('a -> 'b) -> 'a -> 'b end structure PgmlIsabelle : PGML_ISABELLE = struct - open Pgml; - open Pretty; -(* fun pgml_of_prettyT1 (Block(ts,ind,length)) = - Box {orient = SOME HVOrient, indent = SOME ind, content = map pgml_of_prettyT1 ts} +(** print mode **) - | pgml_of_prettyT1 (String (str,len)) = Atoms { kind = NONE, content = [Str str] } - (* TODO: should unquote symbols *) +val pgmlN = "PGML"; +fun pgml_mode f x = setmp print_mode (pgmlN :: ! print_mode) f x; - | pgml_of_prettyT1 (Break (flag,ind)) = Pgml.Break { mandatory = SOME flag, indent = SOME ind } +val _ = Markup.add_mode pgmlN (fn markup as (name, _) => ("", "")); - val pgml_of_prettyT = pgml_of_prettyT1 o dest_prettyT; -*) -end +end;