src/Pure/ProofGeneral/pgml_isabelle.ML
author wenzelm
Sun, 04 Nov 2007 16:43:29 +0100
changeset 25273 189db9ef803f
parent 23935 2a4e42ec9a54
permissions -rw-r--r--
Output.add_mode default prevents escapes from ProofGeneral mode;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23800
ec6f7a398625 added skeleton for print_mode setup;
wenzelm
parents: 23610
diff changeset
     1
(*  Title:      Pure/ProofGeneral/pgml_isabelle.ML
23571
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
     2
    ID:         $Id$
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
     3
    Author:     David Aspinall
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
     4
23800
ec6f7a398625 added skeleton for print_mode setup;
wenzelm
parents: 23610
diff changeset
     5
PGML print mode for common Isabelle markup.
23571
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
     6
*)
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
     7
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
     8
signature PGML_ISABELLE =
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
     9
sig
23800
ec6f7a398625 added skeleton for print_mode setup;
wenzelm
parents: 23610
diff changeset
    10
  val pgml_mode: ('a -> 'b) -> 'a -> 'b
23571
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
    11
end
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
    12
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
    13
structure PgmlIsabelle : PGML_ISABELLE =
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
    14
struct
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
    15
23800
ec6f7a398625 added skeleton for print_mode setup;
wenzelm
parents: 23610
diff changeset
    16
(** print mode **)
23571
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
    17
23800
ec6f7a398625 added skeleton for print_mode setup;
wenzelm
parents: 23610
diff changeset
    18
val pgmlN = "PGML";
23935
2a4e42ec9a54 PrintMode.with_modes;
wenzelm
parents: 23800
diff changeset
    19
fun pgml_mode f x = PrintMode.with_modes [pgmlN] f x;
23571
0cd175710a93 PGML abstraction, draft version
aspinall
parents:
diff changeset
    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
ec6f7a398625 added skeleton for print_mode setup;
wenzelm
parents: 23610
diff changeset
    22
val _ = Markup.add_mode pgmlN (fn markup as (name, _) => ("", ""));
23610
5ade06703b07 Produce good PGML 2.0
aspinall
parents: 23571
diff changeset
    23
23800
ec6f7a398625 added skeleton for print_mode setup;
wenzelm
parents: 23610
diff changeset
    24
end;