--- 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 \
--- 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
--- 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;