--- a/lib/html/isabelle.css Fri Jan 02 22:06:56 2009 +0100
+++ b/lib/html/isabelle.css Fri Jan 02 23:36:35 2009 +0100
@@ -20,20 +20,20 @@
/* inner and outer syntax markup */
-.tfree, tfree { color: purple; }
-.tvar, tvar { color: purple; }
-.free, free { color: blue; }
-.skolem, skolem { color: brown; }
-.bound, bound { color: green; }
-.var, var { color: blue; }
-.num, num { }
-.xnum, xnum { }
-.xstr, xstr { color: brown; }
-.literal, literal { font-weight: bold; }
-
+.tfree, tfree { color: purple; }
+.tvar, tvar { color: purple; }
+.free, free { color: blue; }
+.skolem, skolem { color: brown; }
+.bound, bound { color: green; }
+.var, var { color: blue; }
+.numeral, numeral { }
+.literal, literal { font-weight: bold; }
+.inner_string, inner_string { color: brown; }
+.inner_comment, inner_comment { color: #8B0000; }
+
.loc, loc { color: brown; }
.tclass, tclass { color: red; }
-
+
.keyword, keyword { font-weight: bold; }
.command, command { font-weight: bold; }
.ident, ident { }
--- a/src/HOL/Tools/numeral_syntax.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/numeral_syntax.ML
- ID: $Id$
Authors: Markus Wenzel, TU Muenchen
Concrete syntax for generic numerals -- preserves leading zeros/ones.
@@ -19,12 +18,11 @@
fun mk_bin num =
let
- val {leading_zeros = z, value, ...} = Syntax.read_xnum num;
fun bit b bs = HOLogic.mk_bit b $ bs;
- fun mk 0 = (* FIXME funpow z (bit 0) *) (Syntax.const @{const_name Int.Pls})
- | mk ~1 = (* FIXME funpow z (bit 1) *) (Syntax.const @{const_name Int.Min})
+ fun mk 0 = Syntax.const @{const_name Int.Pls}
+ | mk ~1 = Syntax.const @{const_name Int.Min}
| mk i = let val (q, r) = Integer.div_mod i 2 in bit r (mk q) end;
- in mk value end;
+ in mk (#value (Syntax.read_xnum num)) end;
in
@@ -65,15 +63,18 @@
else sign ^ implode (replicate z "0") ^ num
end;
+fun syntax_numeral t =
+ Syntax.const "_Numeral" $ (Syntax.const "_numeral" $ Syntax.free (dest_bin_str t));
+
in
fun numeral_tr' show_sorts (*"number_of"*) (Type ("fun", [_, T])) (t :: ts) =
- let val t' = Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t) in
- if not (! show_types) andalso can Term.dest_Type T then t'
- else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T
- end
+ let val t' =
+ if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
+ else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
+ in list_comb (t', ts) end
| numeral_tr' _ (*"number_of"*) T (t :: ts) =
- if T = dummyT then Syntax.const "_Numeral" $ Syntax.free (dest_bin_str t)
+ if T = dummyT then list_comb (syntax_numeral t, ts)
else raise Match
| numeral_tr' _ (*"number_of"*) _ _ = raise Match;
--- a/src/HOL/Tools/string_syntax.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/HOL/Tools/string_syntax.ML Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Tools/string_syntax.ML
- ID: $Id$
Author: Makarius
Concrete syntax for hex chars and strings.
@@ -43,8 +42,8 @@
fun dest_char (Syntax.Appl [Syntax.Constant "Char", c1, c2]) = dest_chr c1 c2
| dest_char _ = raise Match;
-fun syntax_xstr cs =
- Syntax.Appl [Syntax.Constant "_xstr", Syntax.Variable (Syntax.implode_xstr cs)];
+fun syntax_string cs =
+ Syntax.Appl [Syntax.Constant "_inner_string", Syntax.Variable (Syntax.implode_xstr cs)];
fun char_ast_tr [Syntax.Variable xstr] =
@@ -53,7 +52,7 @@
| _ => error ("Single character expected: " ^ xstr))
| char_ast_tr asts = raise AST ("char_ast_tr", asts);
-fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_xstr [dest_chr c1 c2]]
+fun char_ast_tr' [c1, c2] = Syntax.Appl [Syntax.Constant "_Char", syntax_string [dest_chr c1 c2]]
| char_ast_tr' _ = raise Match;
@@ -70,7 +69,7 @@
| string_ast_tr asts = raise AST ("string_tr", asts);
fun list_ast_tr' [args] = Syntax.Appl [Syntax.Constant "_String",
- syntax_xstr (map dest_char (Syntax.unfold_ast "_args" args))]
+ syntax_string (map dest_char (Syntax.unfold_ast "_args" args))]
| list_ast_tr' ts = raise Match;
--- a/src/HOLCF/Fixrec.thy Fri Jan 02 22:06:56 2009 +0100
+++ b/src/HOLCF/Fixrec.thy Fri Jan 02 23:36:35 2009 +0100
@@ -216,19 +216,19 @@
syntax
"_pat" :: "'a"
- "_var" :: "'a"
+ "_variable" :: "'a"
"_noargs" :: "'a"
translations
- "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_var p r)"
- "_var (_args x y) r" => "CONST csplit\<cdot>(_var x (_var y r))"
- "_var _noargs r" => "CONST unit_when\<cdot>r"
+ "_Case1 p r" => "CONST branch (_pat p)\<cdot>(_variable p r)"
+ "_variable (_args x y) r" => "CONST csplit\<cdot>(_variable x (_variable y r))"
+ "_variable _noargs r" => "CONST unit_when\<cdot>r"
parse_translation {*
(* rewrites (_pat x) => (return) *)
-(* rewrites (_var x t) => (Abs_CFun (%x. t)) *)
+(* rewrites (_variable x t) => (Abs_CFun (%x. t)) *)
[("_pat", K (Syntax.const "Fixrec.return")),
- mk_binder_tr ("_var", "Abs_CFun")];
+ mk_binder_tr ("_variable", "Abs_CFun")];
*}
text {* Printing Case expressions *}
@@ -250,7 +250,7 @@
val abs = case t of Abs abs => abs
| _ => ("x", dummyT, incr_boundvars 1 t $ Bound 0);
val (x, t') = atomic_abs_tr' abs;
- in (Syntax.const "_var" $ x, t') end
+ in (Syntax.const "_variable" $ x, t') end
| dest_LAM _ = raise Match; (* too few vars: abort translation *)
fun Case1_tr' [Const(@{const_syntax branch},_) $ p, r] =
@@ -261,7 +261,7 @@
*}
translations
- "x" <= "_match Fixrec.return (_var x)"
+ "x" <= "_match Fixrec.return (_variable x)"
subsection {* Pattern combinators for data constructors *}
@@ -320,18 +320,18 @@
text {* Parse translations (variables) *}
translations
- "_var (XCONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
- "_var (XCONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
- "_var (XCONST sinl\<cdot>x) r" => "_var x r"
- "_var (XCONST sinr\<cdot>x) r" => "_var x r"
- "_var (XCONST up\<cdot>x) r" => "_var x r"
- "_var (XCONST TT) r" => "_var _noargs r"
- "_var (XCONST FF) r" => "_var _noargs r"
- "_var (XCONST ONE) r" => "_var _noargs r"
+ "_variable (XCONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
+ "_variable (XCONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
+ "_variable (XCONST sinl\<cdot>x) r" => "_variable x r"
+ "_variable (XCONST sinr\<cdot>x) r" => "_variable x r"
+ "_variable (XCONST up\<cdot>x) r" => "_variable x r"
+ "_variable (XCONST TT) r" => "_variable _noargs r"
+ "_variable (XCONST FF) r" => "_variable _noargs r"
+ "_variable (XCONST ONE) r" => "_variable _noargs r"
translations
- "_var (CONST cpair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
- "_var (CONST spair\<cdot>x\<cdot>y) r" => "_var (_args x y) r"
+ "_variable (CONST cpair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
+ "_variable (CONST spair\<cdot>x\<cdot>y) r" => "_variable (_args x y) r"
text {* Print translations *}
translations
@@ -437,14 +437,14 @@
text {* Parse translations (variables) *}
translations
- "_var _ r" => "_var _noargs r"
- "_var (_as_pat x y) r" => "_var (_args x y) r"
- "_var (_lazy_pat x) r" => "_var x r"
+ "_variable _ r" => "_variable _noargs r"
+ "_variable (_as_pat x y) r" => "_variable (_args x y) r"
+ "_variable (_lazy_pat x) r" => "_variable x r"
text {* Print translations *}
translations
"_" <= "_match (CONST wild_pat) _noargs"
- "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_var x) v)"
+ "_as_pat x (_match p v)" <= "_match (CONST as_pat p) (_args (_variable x) v)"
"_lazy_pat (_match p v)" <= "_match (CONST lazy_pat p) v"
text {* Lazy patterns in lambda abstractions *}
--- a/src/HOLCF/Tools/domain/domain_syntax.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Fri Jan 02 23:36:35 2009 +0100
@@ -89,7 +89,7 @@
fun arg1 n (con,_,args) = foldr cabs (expvar n) (argvars n args);
fun when1 n m = if n = m then arg1 n else K (Constant "UU");
- fun app_var x = mk_appl (Constant "_var") [x, Variable "rhs"];
+ fun app_var x = mk_appl (Constant "_variable") [x, Variable "rhs"];
fun app_pat x = mk_appl (Constant "_pat") [x];
fun args_list [] = Constant "_noargs"
| args_list xs = foldr1 (app "_args") xs;
--- a/src/Pure/General/buffer.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/buffer.ML Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/buffer.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Efficient text buffers.
@@ -10,7 +9,6 @@
type T
val empty: T
val add: string -> T -> T
- val add_substring: substring -> T -> T
val markup: Markup.T -> (T -> T) -> T -> T
val content: T -> string
val output: T -> TextIO.outstream -> unit
@@ -19,46 +17,18 @@
structure Buffer: BUFFER =
struct
-(* datatype *)
-
-datatype T =
- EmptyBuffer
- | String of string * T
- | Substring of substring * T;
+datatype T = Buffer of string list;
-val empty = EmptyBuffer;
-
+val empty = Buffer [];
-(* add content *)
-
-fun add s buf = if s = "" then buf else String (s, buf);
-fun add_substring s buf = if Substring.isEmpty s then buf else Substring (s, buf);
+fun add "" buf = buf
+ | add x (Buffer xs) = Buffer (x :: xs);
fun markup m body =
let val (bg, en) = Markup.output m
in add bg #> body #> add en end;
-
-(* cumulative content *)
-
-fun rev_content EmptyBuffer acc = acc
- | rev_content (String (s, buf)) acc = rev_content buf (s :: acc)
- | rev_content (Substring (s, buf)) acc = rev_content buf (Substring.string s :: acc);
-
-fun content buf = implode (rev_content buf []);
-
-
-(* file output *)
-
-fun rev_buffer EmptyBuffer acc = acc
- | rev_buffer (String (s, buf)) acc = rev_buffer buf (String (s, acc))
- | rev_buffer (Substring (s, buf)) acc = rev_buffer buf (Substring (s, acc));
-
-fun output buffer stream =
- let
- fun rev_output EmptyBuffer = ()
- | rev_output (String (s, buf)) = (TextIO.output (stream, s); rev_output buf)
- | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf);
- in rev_output (rev_buffer buffer empty) end;
+fun content (Buffer xs) = implode (rev xs);
+fun output (Buffer xs) stream = List.app (fn s => TextIO.output (stream, s)) (rev xs);
end;
--- a/src/Pure/General/markup.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/markup.ML Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/General/markup.ML
- ID: $Id$
Author: Makarius
Common markup elements.
@@ -52,11 +51,9 @@
val skolemN: string val skolem: T
val boundN: string val bound: T
val varN: string val var: T
- val numN: string val num: T
- val floatN: string val float: T
- val xnumN: string val xnum: T
- val xstrN: string val xstr: T
+ val numeralN: string val numeral: T
val literalN: string val literal: T
+ val inner_stringN: string val inner_string: T
val inner_commentN: string val inner_comment: T
val sortN: string val sort: T
val typN: string val typ: T
@@ -106,6 +103,7 @@
val debugN: string
val initN: string
val statusN: string
+ val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
val output: T -> output * output
@@ -203,11 +201,9 @@
val (skolemN, skolem) = markup_elem "skolem";
val (boundN, bound) = markup_elem "bound";
val (varN, var) = markup_elem "var";
-val (numN, num) = markup_elem "num";
-val (floatN, float) = markup_elem "float";
-val (xnumN, xnum) = markup_elem "xnum";
-val (xstrN, xstr) = markup_elem "xstr";
+val (numeralN, numeral) = markup_elem "numeral";
val (literalN, literal) = markup_elem "literal";
+val (inner_stringN, inner_string) = markup_elem "inner_string";
val (inner_commentN, inner_comment) = markup_elem "inner_comment";
val (sortN, sort) = markup_elem "sort";
@@ -292,7 +288,8 @@
(* print mode operations *)
-fun default_output (_: T) = ("", "");
+val no_output = ("", "");
+fun default_output (_: T) = no_output;
local
val default = {output = default_output};
@@ -304,7 +301,7 @@
the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
end;
-fun output m = if is_none m then ("", "") else #output (get_mode ()) m;
+fun output m = if is_none m then no_output else #output (get_mode ()) m;
val enclose = output #-> Library.enclose;
--- a/src/Pure/General/symbol.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/symbol.ML Fri Jan 02 23:36:35 2009 +0100
@@ -65,6 +65,7 @@
val bump_string: string -> string
val length: symbol list -> int
val xsymbolsN: string
+ val output: string -> output * int
end;
structure Symbol: SYMBOL =
@@ -175,21 +176,22 @@
ord space <= ord c andalso ord c <= ord "~" andalso c <> "." andalso c <> ">"
orelse ord c >= 128;
-fun encode_raw str =
- let
- val raw0 = enclose "\\<^raw:" ">";
- val raw1 = raw0 o implode;
- val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
-
- fun encode cs = enc (Library.take_prefix raw_chr cs)
- and enc ([], []) = []
- | enc (cs, []) = [raw1 cs]
- | enc ([], d :: ds) = raw2 d :: encode ds
- | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
- in
- if exists_string (not o raw_chr) str then implode (encode (explode str))
- else raw0 str
- end;
+fun encode_raw "" = ""
+ | encode_raw str =
+ let
+ val raw0 = enclose "\\<^raw:" ">";
+ val raw1 = raw0 o implode;
+ val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
+
+ fun encode cs = enc (Library.take_prefix raw_chr cs)
+ and enc ([], []) = []
+ | enc (cs, []) = [raw1 cs]
+ | enc ([], d :: ds) = raw2 d :: encode ds
+ | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds;
+ in
+ if exists_string (not o raw_chr) str then implode (encode (explode str))
+ else raw0 str
+ end;
(* diagnostics *)
@@ -519,9 +521,9 @@
-(** xsymbols **)
+(** symbol output **)
-val xsymbolsN = "xsymbols";
+(* length *)
fun sym_len s =
if not (is_printable s) then (0: int)
@@ -532,8 +534,16 @@
fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
+
+(* print mode *)
+
+val xsymbolsN = "xsymbols";
+
+fun output s = (s, sym_length (sym_explode s));
+
+
(*final declarations of this structure!*)
+val explode = sym_explode;
val length = sym_length;
-val explode = sym_explode;
end;
--- a/src/Pure/General/xml.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/xml.ML Fri Jan 02 23:36:35 2009 +0100
@@ -79,7 +79,7 @@
end;
fun output_markup (markup as (name, atts)) =
- if Markup.is_none markup then ("", "")
+ if Markup.is_none markup then Markup.no_output
else (enclose "<" ">" (elem name atts), enclose "</" ">" name);
--- a/src/Pure/General/yxml.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/General/yxml.ML Fri Jan 02 23:36:35 2009 +0100
@@ -42,7 +42,7 @@
(* output *)
fun output_markup (markup as (name, atts)) =
- if Markup.is_none markup then ("", "")
+ if Markup.is_none markup then Markup.no_output
else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
fun element name atts body =
--- a/src/Pure/Isar/proof_context.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Fri Jan 02 23:36:35 2009 +0100
@@ -408,9 +408,8 @@
("free", free_or_skolem),
("bound", plain_markup Markup.bound),
("var", var_or_skolem),
- ("num", plain_markup Markup.num),
- ("xnum", plain_markup Markup.xnum),
- ("xstr", plain_markup Markup.xstr)];
+ ("numeral", plain_markup Markup.numeral),
+ ("inner_string", plain_markup Markup.inner_string)];
in val _ = Context.>> (Context.map_theory (Sign.add_tokentrfuns token_trans)) end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Jan 02 23:36:35 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/ProofGeneral/proof_general_emacs.ML
- ID: $Id$
Author: David Aspinall and Markus Wenzel
Isabelle/Isar configuration for Emacs Proof General.
@@ -21,81 +20,77 @@
(* print modes *)
val proof_generalN = "ProofGeneralEmacs"; (*token markup (colouring vars, etc.)*)
-val pgasciiN = "PGASCII"; (*plain 7-bit ASCII communication*)
val thm_depsN = "thm_deps"; (*meta-information about theorem deps*)
val test_markupN = "test_markup"; (*XML markup for everything*)
-val _ = Markup.add_mode test_markupN (fn (name, props) =>
- if name = Markup.promptN then ("", "") else XML.output_markup (name, props));
-
-fun special oct =
- if print_mode_active pgasciiN then Symbol.SOH ^ chr (ord (oct_char oct) - 167)
- else oct_char oct;
+fun special ch = Symbol.SOH ^ ch;
-(* text output: print modes for xsymbol *)
+(* render markup *)
local
-fun xsym_output "\\" = "\\\\"
- | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
-
-fun xsymbols_output s =
- if print_mode_active Symbol.xsymbolsN andalso exists_string (fn c => c = "\\") s then
- let val syms = Symbol.explode s
- in (implode (map xsym_output syms), Symbol.length syms) end
- else Output.default_output s;
+fun render_trees ts = fold render_tree ts
+and render_tree (XML.Text s) = Buffer.add s
+ | render_tree (XML.Elem (name, props, ts)) =
+ let
+ val (bg1, en1) =
+ if name <> Markup.promptN andalso print_mode_active test_markupN
+ then XML.output_markup (name, props)
+ else Markup.no_output;
+ val (bg2, en2) =
+ if (case ts of [XML.Text _] => false | _ => true) then Markup.no_output
+ else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
+ else if name = Markup.sendbackN then (special "W", special "X")
+ else if name = Markup.hiliteN then (special "0", special "1")
+ else if name = Markup.tclassN then (special "B", special "A")
+ else if name = Markup.tfreeN then (special "C", special "A")
+ else if name = Markup.tvarN then (special "D", special "A")
+ else if name = Markup.freeN then (special "E", special "A")
+ else if name = Markup.boundN then (special "F", special "A")
+ else if name = Markup.varN then (special "G", special "A")
+ else if name = Markup.skolemN then (special "H", special "A")
+ else Markup.no_output;
+ in
+ Buffer.add bg1 #>
+ Buffer.add bg2 #>
+ render_trees ts #>
+ Buffer.add en2 #>
+ Buffer.add en1
+ end;
in
-fun setup_xsymbols_output () =
- Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
+fun render text =
+ Buffer.content (render_trees (YXML.parse_body text) Buffer.empty);
end;
-(* common markup *)
+(* messages *)
+
+fun message bg en prfx text =
+ (case render text of
+ "" => ()
+ | s => Output.writeln_default (enclose bg en (prefix_lines prfx s)));
-val _ = Markup.add_mode proof_generalN (fn (name, props) =>
- let
- val (bg1, en1) =
- if name = Markup.stateN then (special "366" ^ "\n", "\n" ^ special "367")
- else if name = Markup.sendbackN then (special "376", special "377")
- else if name = Markup.hiliteN then (special "327", special "330")
- else if name = Markup.tclassN then (special "351", special "350")
- else if name = Markup.tfreeN then (special "352", special "350")
- else if name = Markup.tvarN then (special "353", special "350")
- else if name = Markup.freeN then (special "354", special "350")
- else if name = Markup.boundN then (special "355", special "350")
- else if name = Markup.varN then (special "356", special "350")
- else if name = Markup.skolemN then (special "357", special "350")
- else ("", "");
- val (bg2, en2) =
- if name <> Markup.promptN andalso print_mode_active test_markupN
- then XML.output_markup (name, props)
- else ("", "");
- in (bg1 ^ bg2, en2 ^ en1) end);
+fun setup_messages () =
+ (Output.writeln_fn := message "" "" "";
+ Output.status_fn := (fn s => ! Output.priority_fn s);
+ Output.priority_fn := message (special "I") (special "J") "";
+ Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+ Output.debug_fn := message (special "K") (special "L") "+++ ";
+ Output.warning_fn := message (special "K") (special "L") "### ";
+ Output.error_fn := message (special "M") (special "N") "*** ";
+ Output.prompt_fn := (fn s => Output.std_output (render s ^ special "S")));
+
+fun panic s =
+ (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
-(* messages and notification *)
-
-fun decorate bg en prfx =
- Output.writeln_default o enclose bg en o prefix_lines prfx;
+(* notification *)
-fun setup_messages () =
- (Output.writeln_fn := Output.writeln_default;
- Output.status_fn := (fn "" => () | s => ! Output.priority_fn s);
- Output.priority_fn := (fn s => decorate (special "360") (special "361") "" s);
- Output.tracing_fn := (fn s => decorate (special "360" ^ special "375") (special "361") "" s);
- Output.debug_fn := (fn s => decorate (special "362") (special "363") "+++ " s);
- Output.warning_fn := (fn s => decorate (special "362") (special "363") "### " s);
- Output.error_fn := (fn s => decorate (special "364") (special "365") "*** " s);
- Output.prompt_fn := (fn s => Output.std_output (s ^ special "372")));
-
-fun panic s =
- (decorate (special "364") (special "365") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
-
-fun emacs_notify s = decorate (special "360") (special "361") "" s;
+val emacs_notify = message (special "I") (special "J") "";
fun tell_clear_goals () =
emacs_notify "Proof General, please clear the goals buffer.";
@@ -237,7 +232,9 @@
| init true =
(! initialized orelse
(Output.no_warnings init_outer_syntax ();
- setup_xsymbols_output ();
+ Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
+ Output.add_mode proof_generalN Output.default_output Output.default_escape;
+ Markup.add_mode proof_generalN YXML.output_markup;
setup_messages ();
ProofGeneralPgip.init_pgip_channel (! Output.priority_fn);
setup_thy_loader ();
--- a/src/Pure/Syntax/lexicon.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Syntax/lexicon.ML Fri Jan 02 23:36:35 2009 +0100
@@ -169,10 +169,10 @@
| VarSy => Markup.var
| TFreeSy => Markup.tfree
| TVarSy => Markup.tvar
- | NumSy => Markup.num
- | FloatSy => Markup.float
- | XNumSy => Markup.xnum
- | StrSy => Markup.xstr
+ | NumSy => Markup.numeral
+ | FloatSy => Markup.numeral
+ | XNumSy => Markup.numeral
+ | StrSy => Markup.inner_string
| Space => Markup.none
| Comment => Markup.inner_comment
| EOF => Markup.none;
--- a/src/Pure/Syntax/syn_ext.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Fri Jan 02 23:36:35 2009 +0100
@@ -379,7 +379,7 @@
fun stamp_trfun s (c, f) = (c, (f, s));
fun mk_trfun tr = stamp_trfun (stamp ()) tr;
-fun eq_trfun ((_, s1:stamp), (_, s2)) = s1 = s2;
+fun eq_trfun ((_, s1: stamp), (_, s2)) = s1 = s2;
(* token translations *)
@@ -387,7 +387,7 @@
fun tokentrans_mode m trs = map (fn (s, f) => (m, s, f)) trs;
val standard_token_classes =
- ["class", "tfree", "tvar", "free", "bound", "var", "num", "float", "xnum", "xstr"];
+ ["class", "tfree", "tvar", "free", "bound", "var", "numeral", "inner_string"];
val standard_token_markers = map (fn s => "_" ^ s) standard_token_classes;
--- a/src/Pure/Thy/latex.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Thy/latex.ML Fri Jan 02 23:36:35 2009 +0100
@@ -174,7 +174,7 @@
fun latex_markup (s, _) =
if s = Markup.keywordN then ("\\isakeyword{", "}")
else if s = Markup.commandN then ("\\isacommand{", "}")
- else ("", "");
+ else Markup.no_output;
fun latex_indent "" _ = ""
| latex_indent s _ = enclose "\\isaindent{" "}" s;
--- a/src/Pure/Thy/thy_syntax.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Fri Jan 02 23:36:35 2009 +0100
@@ -58,9 +58,9 @@
| T.Ident => Markup.ident
| T.LongIdent => Markup.ident
| T.SymIdent => Markup.ident
- | T.Var => Markup.ident
- | T.TypeIdent => Markup.ident
- | T.TypeVar => Markup.ident
+ | T.Var => Markup.var
+ | T.TypeIdent => Markup.tfree
+ | T.TypeVar => Markup.tvar
| T.Nat => Markup.ident
| T.String => Markup.string
| T.AltString => Markup.altstring
--- a/src/Pure/Tools/isabelle_process.ML Fri Jan 02 22:06:56 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.ML Fri Jan 02 23:36:35 2009 +0100
@@ -1,15 +1,14 @@
(* Title: Pure/Tools/isabelle_process.ML
- ID: $Id$
Author: Makarius
Isabelle process wrapper -- interaction via external program.
General format of process output:
- (a) unmarked stdout/stderr, no line structure (output should be
+ (1) unmarked stdout/stderr, no line structure (output should be
processed immediately as it arrives);
- (b) properly marked-up messages, e.g. for writeln channel
+ (2) properly marked-up messages, e.g. for writeln channel
"\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
@@ -17,13 +16,14 @@
each, and the remaining text is any number of lines (output is
supposed to be processed in one piece);
- (c) special init message holds "pid" and "session" property.
+ (3) special init message holds "pid" and "session" property;
+
+ (4) message content is encoded in YXML format.
*)
signature ISABELLE_PROCESS =
sig
val isabelle_processN: string
- val xmlN: string
val init: string -> unit
end;
@@ -33,7 +33,6 @@
(* print modes *)
val isabelle_processN = "isabelle_process";
-val xmlN = "XML";
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
@@ -56,19 +55,14 @@
let val clean = clean_string [Symbol.STX, "\n", "\r"]
in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
-fun message_text class ts =
- let
- val doc = XML.Elem (Markup.messageN, [(Markup.classN, class)], ts);
- val msg =
- if print_mode_active xmlN then XML.header ^ XML.string_of doc
- else YXML.string_of doc;
- in clean_string [Symbol.STX] msg end;
+fun message_text class body =
+ YXML.element Markup.messageN [(Markup.classN, class)] [clean_string [Symbol.STX] body];
-fun message_pos ts = get_first get_pos ts
-and get_pos (elem as XML.Elem (name, atts, ts)) =
- if name = Markup.positionN then SOME (Position.of_properties atts)
- else message_pos ts
- | get_pos _ = NONE;
+fun message_pos trees = trees |> get_first
+ (fn XML.Elem (name, atts, ts) =>
+ if name = Markup.positionN then SOME (Position.of_properties atts)
+ else message_pos ts
+ | _ => NONE);
fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
(TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
@@ -78,19 +72,18 @@
fun message _ _ _ "" = ()
| message out_stream ch class body =
let
- val (txt, pos) =
- let val ts = YXML.parse_body body
- in (message_text class ts, the_default Position.none (message_pos ts)) end;
+ val pos = the_default Position.none (message_pos (YXML.parse_body body));
val props =
Position.properties_of (Position.thread_data ())
|> Position.default_properties pos;
+ val txt = message_text class body;
in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
fun init_message out_stream =
let
val pid = (Markup.pidN, process_id ());
val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
- val text = message_text Markup.initN [XML.Text (Session.welcome ())];
+ val text = message_text Markup.initN (Session.welcome ());
in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
end;