src/Pure/ProofGeneral/pgml_isabelle.ML
author wenzelm
Fri Jun 13 21:04:42 2008 +0200 (2008-06-13)
changeset 27195 bbf4cbc69243
parent 25273 189db9ef803f
permissions -rw-r--r--
map_const: soft version, no failure here;
wenzelm@23800
     1
(*  Title:      Pure/ProofGeneral/pgml_isabelle.ML
aspinall@23571
     2
    ID:         $Id$
aspinall@23571
     3
    Author:     David Aspinall
aspinall@23571
     4
wenzelm@23800
     5
PGML print mode for common Isabelle markup.
aspinall@23571
     6
*)
aspinall@23571
     7
aspinall@23571
     8
signature PGML_ISABELLE =
aspinall@23571
     9
sig
wenzelm@23800
    10
  val pgml_mode: ('a -> 'b) -> 'a -> 'b
aspinall@23571
    11
end
aspinall@23571
    12
aspinall@23571
    13
structure PgmlIsabelle : PGML_ISABELLE =
aspinall@23571
    14
struct
aspinall@23571
    15
wenzelm@23800
    16
(** print mode **)
aspinall@23571
    17
wenzelm@23800
    18
val pgmlN = "PGML";
wenzelm@23935
    19
fun pgml_mode f x = PrintMode.with_modes [pgmlN] f x;
aspinall@23571
    20
wenzelm@25273
    21
val _ = Output.add_mode pgmlN Output.default_output Output.default_escape;
wenzelm@23800
    22
val _ = Markup.add_mode pgmlN (fn markup as (name, _) => ("", ""));
aspinall@23610
    23
wenzelm@23800
    24
end;