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;