author | wenzelm |
Fri, 15 Aug 2008 15:50:52 +0200 | |
changeset 27885 | 76b51cd0a37c |
parent 25273 | 189db9ef803f |
permissions | -rw-r--r-- |
23800 | 1 |
(* Title: Pure/ProofGeneral/pgml_isabelle.ML |
23571 | 2 |
ID: $Id$ |
3 |
Author: David Aspinall |
|
4 |
||
23800 | 5 |
PGML print mode for common Isabelle markup. |
23571 | 6 |
*) |
7 |
||
8 |
signature PGML_ISABELLE = |
|
9 |
sig |
|
23800 | 10 |
val pgml_mode: ('a -> 'b) -> 'a -> 'b |
23571 | 11 |
end |
12 |
||
13 |
structure PgmlIsabelle : PGML_ISABELLE = |
|
14 |
struct |
|
15 |
||
23800 | 16 |
(** print mode **) |
23571 | 17 |
|
23800 | 18 |
val pgmlN = "PGML"; |
23935 | 19 |
fun pgml_mode f x = PrintMode.with_modes [pgmlN] f x; |
23571 | 20 |
|
25273
189db9ef803f
Output.add_mode default prevents escapes from ProofGeneral mode;
wenzelm
parents:
23935
diff
changeset
|
21 |
val _ = Output.add_mode pgmlN Output.default_output Output.default_escape; |
23800 | 22 |
val _ = Markup.add_mode pgmlN (fn markup as (name, _) => ("", "")); |
23610 | 23 |
|
23800 | 24 |
end; |