1.1 --- a/src/Pure/IsaMakefile	Wed Aug 27 23:46:33 2008 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Thu Aug 28 00:33:04 2008 +0200
     1.3 @@ -62,8 +62,7 @@
     1.4    ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
     1.5    ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
     1.6    ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
     1.7 -  ProofGeneral/pgml_isabelle.ML ProofGeneral/preferences.ML		\
     1.8 -  ProofGeneral/proof_general_emacs.ML					\
     1.9 +  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
    1.10    ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
    1.11    Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
    1.12    Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\

     2.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Wed Aug 27 23:46:33 2008 +0200
     2.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Thu Aug 28 00:33:04 2008 +0200
     2.3 @@ -14,7 +14,6 @@
     2.4  use "pgip.ML";
     2.5  
     2.6  use "pgip_isabelle.ML";
     2.7 -use "pgml_isabelle.ML";
     2.8  
     2.9  (use
    2.10    |> setmp Proofterm.proofs 1

     3.1 --- a/src/Pure/ProofGeneral/pgml_isabelle.ML	Wed Aug 27 23:46:33 2008 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,24 +0,0 @@
     3.4 -(*  Title:      Pure/ProofGeneral/pgml_isabelle.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     David Aspinall
     3.7 -
     3.8 -PGML print mode for common Isabelle markup.
     3.9 -*)
    3.10 -
    3.11 -signature PGML_ISABELLE =
    3.12 -sig
    3.13 -  val pgml_mode: ('a -> 'b) -> 'a -> 'b
    3.14 -end
    3.15 -
    3.16 -structure PgmlIsabelle : PGML_ISABELLE =
    3.17 -struct
    3.18 -
    3.19 -(** print mode **)
    3.20 -
    3.21 -val pgmlN = "PGML";
    3.22 -fun pgml_mode f x = PrintMode.with_modes [pgmlN] f x;
    3.23 -
    3.24 -val _ = Output.add_mode pgmlN Output.default_output Output.default_escape;
    3.25 -val _ = Markup.add_mode pgmlN (fn markup as (name, _) => ("", ""));
    3.26 -
    3.27 -end;