# HG changeset patch
# User wenzelm
# Date 1219876384 -7200
# Node ID 8b197e2bc66a07b74084465830ad6a466e43ad95
# Parent  4c55cdec4ce7bf39870e0b655e8cef896787c606
removed obsolete ProofGeneral/pgml_isabelle.ML;

diff -r 4c55cdec4ce7 -r 8b197e2bc66a src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Wed Aug 27 23:46:33 2008 +0200
+++ b/src/Pure/IsaMakefile	Thu Aug 28 00:33:04 2008 +0200
@@ -62,8 +62,7 @@
   ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
   ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
   ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
-  ProofGeneral/pgml_isabelle.ML ProofGeneral/preferences.ML		\
-  ProofGeneral/proof_general_emacs.ML					\
+  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
   ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
   Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
   Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
diff -r 4c55cdec4ce7 -r 8b197e2bc66a src/Pure/ProofGeneral/ROOT.ML
--- a/src/Pure/ProofGeneral/ROOT.ML	Wed Aug 27 23:46:33 2008 +0200
+++ b/src/Pure/ProofGeneral/ROOT.ML	Thu Aug 28 00:33:04 2008 +0200
@@ -14,7 +14,6 @@
 use "pgip.ML";
 
 use "pgip_isabelle.ML";
-use "pgml_isabelle.ML";
 
 (use
   |> setmp Proofterm.proofs 1
diff -r 4c55cdec4ce7 -r 8b197e2bc66a src/Pure/ProofGeneral/pgml_isabelle.ML
--- a/src/Pure/ProofGeneral/pgml_isabelle.ML	Wed Aug 27 23:46:33 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-(*  Title:      Pure/ProofGeneral/pgml_isabelle.ML
-    ID:         $Id$
-    Author:     David Aspinall
-
-PGML print mode for common Isabelle markup.
-*)
-
-signature PGML_ISABELLE =
-sig
-  val pgml_mode: ('a -> 'b) -> 'a -> 'b
-end
-
-structure PgmlIsabelle : PGML_ISABELLE =
-struct
-
-(** print mode **)
-
-val pgmlN = "PGML";
-fun pgml_mode f x = PrintMode.with_modes [pgmlN] f x;
-
-val _ = Output.add_mode pgmlN Output.default_output Output.default_escape;
-val _ = Markup.add_mode pgmlN (fn markup as (name, _) => ("", ""));
-
-end;