--- a/Admin/isatest/settings/at-mac-poly-5.1-para Sat Jan 03 08:39:18 2009 +0100
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para Sat Jan 03 08:39:54 2009 +0100
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-5.2.1"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--immutable 800 --mutable 1200"
+ ML_OPTIONS="--mutable 500 --immutable 1500"
ISABELLE_HOME_USER=~/isabelle-at-mac-poly-e
--- a/lib/html/isabelle.css Sat Jan 03 08:39:18 2009 +0100
+++ b/lib/html/isabelle.css Sat Jan 03 08:39:54 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/function_package/context_tree.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML Sat Jan 03 08:39:54 2009 +0100
@@ -80,7 +80,7 @@
let
val t' = snd (dest_all_all t)
val (assumes, concl) = Logic.strip_horn t'
- in (fold (curry OldTerm.add_term_vars) assumes [], OldTerm.term_vars concl)
+ in (fold Term.add_vars assumes [], Term.add_vars concl [])
end
fun cong_deps crule =
@@ -89,7 +89,9 @@
in
IntGraph.empty
|> fold (fn (i,_)=> IntGraph.new_node (i,i)) num_branches
- |> fold_product (fn (i,(c1,_)) => fn (j,(_, t2)) => if i = j orelse null (c1 inter t2) then I else IntGraph.add_edge_acyclic (i,j))
+ |> fold_product (fn (i, (c1, _)) => fn (j, (_, t2)) =>
+ if i = j orelse null (c1 inter t2)
+ then I else IntGraph.add_edge_acyclic (i,j))
num_branches num_branches
end
--- a/src/HOL/Tools/function_package/fundef_core.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML Sat Jan 03 08:39:54 2009 +0100
@@ -436,7 +436,7 @@
|> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
|> forall_intr (cterm_of thy x)
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *)
- |> (fn it => fold (forall_intr o cterm_of thy) (OldTerm.term_vars (prop_of it)) it)
+ |> (fn it => fold (forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it)
val goalstate = Conjunction.intr graph_is_function complete
|> Thm.close_derivation
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Sat Jan 03 08:39:54 2009 +0100
@@ -63,9 +63,10 @@
fun inst_case_thm thy x P thm =
let
- val [Pv, xv] = OldTerm.term_vars (prop_of thm)
+ val [Pv, xv] = Term.add_vars (prop_of thm) []
in
- cterm_instantiate [(cterm_of thy xv, cterm_of thy x), (cterm_of thy Pv, cterm_of thy P)] thm
+ cterm_instantiate [(cterm_of thy (Var xv), cterm_of thy x),
+ (cterm_of thy (Var Pv), cterm_of thy P)] thm
end
--- a/src/HOL/Tools/numeral_syntax.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/HOL/Tools/string_syntax.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/HOLCF/Fixrec.thy Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/General/buffer.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/General/markup.ML Sat Jan 03 08:39:54 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/position.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/General/position.ML Sat Jan 03 08:39:54 2009 +0100
@@ -1,8 +1,7 @@
(* Title: Pure/General/position.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
-Source positions: counting Isabelle symbols -- starting from 1.
+Source positions: counting Isabelle symbols, starting from 1.
*)
signature POSITION =
@@ -19,6 +18,7 @@
val file: string -> T
val line: int -> T
val line_file: int -> string -> T
+ val id: string -> T
val get_id: T -> string option
val put_id: string -> T -> T
val of_properties: Properties.T -> T
@@ -86,6 +86,7 @@
val none = Pos ((0, 0, 0), []);
val start = Pos ((1, 1, 1), []);
+
fun file_name "" = []
| file_name name = [(Markup.fileN, name)];
@@ -95,11 +96,14 @@
fun line i = line_file i "";
-(* markup properties *)
+fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]);
fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
+
+(* markup properties *)
+
fun of_properties props =
let
fun get name =
--- a/src/Pure/General/symbol.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/General/symbol.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/General/xml.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/General/yxml.ML Sat Jan 03 08:39:54 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/IsaMakefile Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/IsaMakefile Sat Jan 03 08:39:54 2009 +0100
@@ -48,15 +48,15 @@
Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML \
Isar/spec_parse.ML Isar/specification.ML Isar/subclass.ML \
- Isar/theory_target.ML Isar/toplevel.ML ML-Systems/alice.ML \
- ML-Systems/exn.ML ML-Systems/install_pp_polyml.ML \
- ML-Systems/ml_name_space.ML ML-Systems/multithreading.ML \
- ML-Systems/mosml.ML ML-Systems/multithreading_polyml.ML \
- ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \
- ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML \
- ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
- ML-Systems/polyml_common.ML ML-Systems/polyml.ML \
- ML-Systems/polyml_old_compiler4.ML \
+ Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \
+ ML-Systems/alice.ML ML-Systems/exn.ML \
+ ML-Systems/install_pp_polyml.ML ML-Systems/ml_name_space.ML \
+ ML-Systems/multithreading.ML ML-Systems/mosml.ML \
+ ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML \
+ ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML \
+ ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML \
+ ML-Systems/polyml-5.1.ML ML-Systems/polyml_common.ML \
+ ML-Systems/polyml.ML ML-Systems/polyml_old_compiler4.ML \
ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML \
ML-Systems/smlnj.ML ML-Systems/system_shell.ML \
ML-Systems/time_limit.ML ML-Systems/thread_dummy.ML \
@@ -74,8 +74,8 @@
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \
- Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
- Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML \
+ Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML \
+ Thy/thy_syntax.ML Tools/ROOT.ML Tools/invoke.ML \
Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML \
assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \
consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \
--- a/src/Pure/Isar/ROOT.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Isar/ROOT.ML Sat Jan 03 08:39:54 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/ROOT.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Isar -- Intelligible Semi-Automated Reasoning for Isabelle.
@@ -21,8 +20,9 @@
(*outer syntax*)
use "outer_lex.ML";
+use "outer_keyword.ML";
use "outer_parse.ML";
-use "outer_keyword.ML";
+use "value_parse.ML";
use "args.ML";
use "antiquote.ML";
use "../ML/ml_context.ML";
@@ -80,7 +80,7 @@
(*theory syntax*)
use "../Thy/term_style.ML";
use "../Thy/thy_output.ML";
-use "../Thy/thy_edit.ML";
+use "../Thy/thy_syntax.ML";
use "../old_goals.ML";
use "outer_syntax.ML";
use "../Thy/thy_info.ML";
--- a/src/Pure/Isar/isar.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Isar/isar.ML Sat Jan 03 08:39:54 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/isar.ML
- ID: $Id$
Author: Makarius
The global Isabelle/Isar state and main read-eval-print loop.
@@ -41,15 +40,6 @@
type id = string;
val no_id : id = "";
-fun identify tr =
- (case Toplevel.get_id tr of
- SOME id => (id, tr)
- | NONE =>
- let val id =
- if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of tr ^ serial_string ()
- else "isabelle:" ^ serial_string ()
- in (id, Toplevel.put_id id tr) end);
-
(* command category *)
@@ -168,7 +158,15 @@
fun create_command raw_tr =
let
- val (id, tr) = identify raw_tr;
+ val (id, tr) =
+ (case Toplevel.get_id raw_tr of
+ SOME id => (id, raw_tr)
+ | NONE =>
+ let val id =
+ if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
+ else "isabelle:" ^ serial_string ()
+ in (id, Toplevel.put_id id raw_tr) end);
+
val cmd = make_command (category_of tr, tr, Unprocessed);
val _ = change_commands (Graph.new_node (id, cmd));
in id end;
@@ -377,26 +375,25 @@
local
-structure P = OuterParse and K = OuterKeyword;
+structure P = struct open OuterParse open ValueParse end;
val op >> = Scan.>>;
in
val _ =
- OuterSyntax.improper_command "Isar.command" "define command (Isar editor model)" K.control
- (P.props_text >> (fn (pos, str) =>
- Toplevel.no_timing o Toplevel.imperative (fn () =>
- ignore (create_command (OuterSyntax.prepare_command pos str)))));
+ OuterSyntax.internal_command "Isar.command"
+ (P.string -- P.string >> (fn (id, text) =>
+ Toplevel.imperative (fn () =>
+ ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
val _ =
- OuterSyntax.improper_command "Isar.insert" "insert command (Isar editor model)" K.control
+ OuterSyntax.internal_command "Isar.insert"
(P.string -- P.string >> (fn (prev, id) =>
- Toplevel.no_timing o Toplevel.imperative (fn () => insert_command prev id)));
+ Toplevel.imperative (fn () => insert_command prev id)));
val _ =
- OuterSyntax.improper_command "Isar.remove" "remove command (Isar editor model)" K.control
- (P.string >> (fn id =>
- Toplevel.no_timing o Toplevel.imperative (fn () => remove_command id)));
+ OuterSyntax.internal_command "Isar.remove"
+ (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
end;
--- a/src/Pure/Isar/isar.scala Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Isar/isar.scala Sat Jan 03 08:39:54 2009 +0100
@@ -1,22 +1,19 @@
/* Title: Pure/Isar/isar.scala
Author: Makarius
-Isar toplevel editor model.
+Isar document model.
*/
package isabelle
-import java.util.Properties
-
class Isar(isabelle_system: IsabelleSystem, results: EventBus[IsabelleProcess.Result], args: String*)
extends IsabelleProcess(isabelle_system, results, args: _*)
{
-
/* basic editor commands */
- def create_command(props: Properties, text: String) =
- output_sync("Isar.command " + IsabelleSyntax.encode_properties(props) + " " +
+ def create_command(id: String, text: String) =
+ output_sync("Isar.command " + IsabelleSyntax.encode_string(id) + " " +
IsabelleSyntax.encode_string(text))
def insert_command(prev: String, id: String) =
@@ -25,5 +22,4 @@
def remove_command(id: String) =
output_sync("Isar.remove " + IsabelleSyntax.encode_string(id))
-
}
--- a/src/Pure/Isar/isar_syn.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Jan 03 08:39:54 2009 +0100
@@ -757,9 +757,13 @@
(* nested commands *)
+val props_text =
+ Scan.optional ValueParse.properties [] -- P.position P.string >> (fn (props, (str, pos)) =>
+ (Position.of_properties (Position.default_properties pos props), str));
+
val _ =
OuterSyntax.improper_command "Isabelle.command" "nested Isabelle command" K.control
- (P.props_text :|-- (fn (pos, str) =>
+ (props_text :|-- (fn (pos, str) =>
(case OuterSyntax.parse pos str of
[tr] => Scan.succeed (K tr)
| _ => Scan.fail_with (K "exactly one command expected"))
--- a/src/Pure/Isar/outer_parse.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML Sat Jan 03 08:39:54 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/outer_parse.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
Generic parsers for Isabelle/Isar outer syntax.
@@ -8,48 +7,49 @@
signature OUTER_PARSE =
sig
type token = OuterLex.token
+ type 'a parser = token list -> 'a * token list
val group: string -> (token list -> 'a) -> token list -> 'a
val !!! : (token list -> 'a) -> token list -> 'a
val !!!! : (token list -> 'a) -> token list -> 'a
val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
- val not_eof: token list -> token * token list
+ val not_eof: token parser
val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b
- val command: token list -> string * token list
- val keyword: token list -> string * token list
- val short_ident: token list -> string * token list
- val long_ident: token list -> string * token list
- val sym_ident: token list -> string * token list
- val minus: token list -> string * token list
- val term_var: token list -> string * token list
- val type_ident: token list -> string * token list
- val type_var: token list -> string * token list
- val number: token list -> string * token list
- val string: token list -> string * token list
- val alt_string: token list -> string * token list
- val verbatim: token list -> string * token list
- val sync: token list -> string * token list
- val eof: token list -> string * token list
- val keyword_with: (string -> bool) -> token list -> string * token list
- val keyword_ident_or_symbolic: token list -> string * token list
- val $$$ : string -> token list -> string * token list
- val reserved: string -> token list -> string * token list
- val semicolon: token list -> string * token list
- val underscore: token list -> string * token list
- val maybe: (token list -> 'a * token list) -> token list -> 'a option * token list
- val tag_name: token list -> string * token list
- val tags: token list -> string list * token list
- val opt_unit: token list -> unit * token list
- val opt_keyword: string -> token list -> bool * token list
- val begin: token list -> string * token list
- val opt_begin: token list -> bool * token list
- val nat: token list -> int * token list
- val int: token list -> int * token list
- val enum: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
- val enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
- val and_list: (token list -> 'a * token list) -> token list -> 'a list * token list
- val and_list1: (token list -> 'a * token list) -> token list -> 'a list * token list
+ val command: string parser
+ val keyword: string parser
+ val short_ident: string parser
+ val long_ident: string parser
+ val sym_ident: string parser
+ val minus: string parser
+ val term_var: string parser
+ val type_ident: string parser
+ val type_var: string parser
+ val number: string parser
+ val string: string parser
+ val alt_string: string parser
+ val verbatim: string parser
+ val sync: string parser
+ val eof: string parser
+ val keyword_with: (string -> bool) -> string parser
+ val keyword_ident_or_symbolic: string parser
+ val $$$ : string -> string parser
+ val reserved: string -> string parser
+ val semicolon: string parser
+ val underscore: string parser
+ val maybe: 'a parser -> 'a option parser
+ val tag_name: string parser
+ val tags: string list parser
+ val opt_unit: unit parser
+ val opt_keyword: string -> bool parser
+ val begin: string parser
+ val opt_begin: bool parser
+ val nat: int parser
+ val int: int parser
+ val enum: string -> 'a parser -> 'a list parser
+ val enum1: string -> 'a parser -> 'a list parser
+ val and_list: 'a parser -> 'a list parser
+ val and_list1: 'a parser -> 'a list parser
val enum': string -> ('a * token list -> 'b * ('a * token list)) ->
'a * token list -> 'b list * ('a * token list)
val enum1': string -> ('a * token list -> 'b * ('a * token list)) ->
@@ -58,46 +58,44 @@
'a * token list -> 'b list * ('a * token list)
val and_list1': ('a * token list -> 'b * ('a * token list)) ->
'a * token list -> 'b list * ('a * token list)
- val list: (token list -> 'a * token list) -> token list -> 'a list * token list
- val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
- val name: token list -> bstring * token list
- val binding: token list -> Binding.T * token list
- val xname: token list -> xstring * token list
- val text: token list -> string * token list
- val path: token list -> Path.T * token list
- val parname: token list -> string * token list
- val parbinding: token list -> Binding.T * token list
- val sort: token list -> string * token list
- val arity: token list -> (string * string list * string) * token list
- val multi_arity: token list -> (string list * string list * string) * token list
- val type_args: token list -> string list * token list
- val typ_group: token list -> string * token list
- val typ: token list -> string * token list
- val mixfix: token list -> mixfix * token list
- val mixfix': token list -> mixfix * token list
- val opt_infix: token list -> mixfix * token list
- val opt_infix': token list -> mixfix * token list
- val opt_mixfix: token list -> mixfix * token list
- val opt_mixfix': token list -> mixfix * token list
- val where_: token list -> string * token list
- val const: token list -> (string * string * mixfix) * token list
- val params: token list -> (Binding.T * string option) list * token list
- val simple_fixes: token list -> (Binding.T * string option) list * token list
- val fixes: token list -> (Binding.T * string option * mixfix) list * token list
- val for_fixes: token list -> (Binding.T * string option * mixfix) list * token list
- val for_simple_fixes: token list -> (Binding.T * string option) list * token list
- val ML_source: token list -> (SymbolPos.text * Position.T) * token list
- val doc_source: token list -> (SymbolPos.text * Position.T) * token list
- val properties: token list -> Properties.T * token list
- val props_text: token list -> (Position.T * string) * token list
- val term_group: token list -> string * token list
- val prop_group: token list -> string * token list
- val term: token list -> string * token list
- val prop: token list -> string * token list
- val propp: token list -> (string * string list) * token list
- val termp: token list -> (string * string list) * token list
- val target: token list -> xstring * token list
- val opt_target: token list -> xstring option * token list
+ val list: 'a parser -> 'a list parser
+ val list1: 'a parser -> 'a list parser
+ val name: bstring parser
+ val binding: Binding.T parser
+ val xname: xstring parser
+ val text: string parser
+ val path: Path.T parser
+ val parname: string parser
+ val parbinding: Binding.T parser
+ val sort: string parser
+ val arity: (string * string list * string) parser
+ val multi_arity: (string list * string list * string) parser
+ val type_args: string list parser
+ val typ_group: string parser
+ val typ: string parser
+ val mixfix: mixfix parser
+ val mixfix': mixfix parser
+ val opt_infix: mixfix parser
+ val opt_infix': mixfix parser
+ val opt_mixfix: mixfix parser
+ val opt_mixfix': mixfix parser
+ val where_: string parser
+ val const: (string * string * mixfix) parser
+ val params: (Binding.T * string option) list parser
+ val simple_fixes: (Binding.T * string option) list parser
+ val fixes: (Binding.T * string option * mixfix) list parser
+ val for_fixes: (Binding.T * string option * mixfix) list parser
+ val for_simple_fixes: (Binding.T * string option) list parser
+ val ML_source: (SymbolPos.text * Position.T) parser
+ val doc_source: (SymbolPos.text * Position.T) parser
+ val term_group: string parser
+ val prop_group: string parser
+ val term: string parser
+ val prop: string parser
+ val propp: (string * string list) parser
+ val termp: (string * string list) parser
+ val target: xstring parser
+ val opt_target: xstring option parser
end;
structure OuterParse: OUTER_PARSE =
@@ -106,6 +104,8 @@
structure T = OuterLex;
type token = T.token;
+type 'a parser = token list -> 'a * token list;
+
(** error handling **)
@@ -310,12 +310,6 @@
val ML_source = source_position (group "ML source" text);
val doc_source = source_position (group "document source" text);
-val properties = $$$ "(" |-- !!! (list1 (string -- ($$$ "=" |-- string)) --| $$$ ")");
-
-val props_text =
- Scan.optional properties [] -- position string >> (fn (props, (str, pos)) =>
- (Position.of_properties (Position.default_properties pos props), str));
-
(* terms *)
--- a/src/Pure/Isar/outer_syntax.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Sat Jan 03 08:39:54 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/outer_syntax.ML
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
The global Isabelle/Isar outer syntax.
@@ -10,17 +9,20 @@
signature OUTER_SYNTAX =
sig
- type parser_fn = OuterLex.token list ->
- (Toplevel.transition -> Toplevel.transition) * OuterLex.token list
- val command: string -> string -> OuterKeyword.T -> parser_fn -> unit
- val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T -> parser_fn -> unit
- val improper_command: string -> string -> OuterKeyword.T -> parser_fn -> unit
+ type 'a parser = 'a OuterParse.parser
+ val command: string -> string -> OuterKeyword.T ->
+ (Toplevel.transition -> Toplevel.transition) parser -> unit
+ val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
+ (Toplevel.transition -> Toplevel.transition) parser -> unit
+ val improper_command: string -> string -> OuterKeyword.T ->
+ (Toplevel.transition -> Toplevel.transition) parser -> unit
+ val internal_command: string -> (Toplevel.transition -> Toplevel.transition) parser -> unit
val local_theory: string -> string -> OuterKeyword.T ->
- (OuterParse.token list -> (local_theory -> local_theory) * OuterLex.token list) -> unit
+ (local_theory -> local_theory) parser -> unit
val local_theory_to_proof': string -> string -> OuterKeyword.T ->
- (OuterParse.token list -> (bool -> local_theory -> Proof.state) * OuterLex.token list) -> unit
+ (bool -> local_theory -> Proof.state) parser -> unit
val local_theory_to_proof: string -> string -> OuterKeyword.T ->
- (OuterParse.token list -> (local_theory -> Proof.state) * OuterLex.token list) -> unit
+ (local_theory -> Proof.state) parser -> unit
val print_outer_syntax: unit -> unit
val scan: Position.T -> string -> OuterLex.token list
val parse: Position.T -> string -> Toplevel.transition list
@@ -36,22 +38,22 @@
structure T = OuterLex;
structure P = OuterParse;
+type 'a parser = 'a P.parser;
+
(** outer syntax **)
-(* parsers *)
+(* command parsers *)
-type parser_fn = T.token list -> (Toplevel.transition -> Toplevel.transition) * T.token list;
-
-datatype parser = Parser of
+datatype command = Command of
{comment: string,
markup: ThyOutput.markup option,
int_only: bool,
- parse: parser_fn};
+ parse: (Toplevel.transition -> Toplevel.transition) parser};
-fun make_parser comment markup int_only parse =
- Parser {comment = comment, markup = markup, int_only = int_only, parse = parse};
+fun make_command comment markup int_only parse =
+ Command {comment = comment, markup = markup, int_only = int_only, parse = parse};
(* parse command *)
@@ -63,7 +65,7 @@
fun body cmd (name, _) =
(case cmd name of
- SOME (Parser {int_only, parse, ...}) =>
+ SOME (Command {int_only, parse, ...}) =>
P.!!! (Scan.prompt (name ^ "# ") (P.tags |-- parse >> pair int_only))
| NONE => sys_error ("no parser for outer syntax command " ^ quote name));
@@ -85,47 +87,50 @@
local
-val global_parsers = ref (Symtab.empty: parser Symtab.table);
+val global_commands = ref (Symtab.empty: command Symtab.table);
val global_markups = ref ([]: (string * ThyOutput.markup) list);
-fun change_parsers f = CRITICAL (fn () =>
- (change global_parsers f;
+fun change_commands f = CRITICAL (fn () =>
+ (change global_commands f;
global_markups :=
- Symtab.fold (fn (name, Parser {markup = SOME m, ...}) => cons (name, m) | _ => I)
- (! global_parsers) []));
+ Symtab.fold (fn (name, Command {markup = SOME m, ...}) => cons (name, m) | _ => I)
+ (! global_commands) []));
in
(* access current syntax *)
-fun get_parsers () = CRITICAL (fn () => ! global_parsers);
+fun get_commands () = CRITICAL (fn () => ! global_commands);
fun get_markups () = CRITICAL (fn () => ! global_markups);
-fun get_parser () = Symtab.lookup (get_parsers ());
-fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_parser ()));
+fun get_command () = Symtab.lookup (get_commands ());
+fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
fun is_markup kind name = AList.lookup (op =) (get_markups ()) name = SOME kind;
(* augment syntax *)
-fun add_parser name kind parser = CRITICAL (fn () =>
+fun add_command name kind cmd = CRITICAL (fn () =>
(OuterKeyword.command name kind;
- if not (Symtab.defined (get_parsers ()) name) then ()
+ if not (Symtab.defined (get_commands ()) name) then ()
else warning ("Redefining outer syntax command " ^ quote name);
- change_parsers (Symtab.update (name, parser))));
+ change_commands (Symtab.update (name, cmd))));
fun command name comment kind parse =
- add_parser name kind (make_parser comment NONE false parse);
+ add_command name kind (make_command comment NONE false parse);
fun markup_command markup name comment kind parse =
- add_parser name kind (make_parser comment (SOME markup) false parse);
+ add_command name kind (make_command comment (SOME markup) false parse);
fun improper_command name comment kind parse =
- add_parser name kind (make_parser comment NONE true parse);
+ add_command name kind (make_command comment NONE true parse);
end;
+fun internal_command name parse =
+ command name "(internal)" OuterKeyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
+
(* local_theory commands *)
@@ -133,22 +138,22 @@
command name comment kind (P.opt_target -- parse
>> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
-val local_theory = local_theory_command false Toplevel.local_theory;
+val local_theory = local_theory_command false Toplevel.local_theory;
val local_theory_to_proof' = local_theory_command true Toplevel.local_theory_to_proof';
-val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
+val local_theory_to_proof = local_theory_command true Toplevel.local_theory_to_proof;
(* inspect syntax *)
-fun dest_parsers () =
- get_parsers () |> Symtab.dest |> sort_wrt #1
- |> map (fn (name, Parser {comment, int_only, ...}) => (name, comment, int_only));
+fun dest_commands () =
+ get_commands () |> Symtab.dest |> sort_wrt #1
+ |> map (fn (name, Command {comment, int_only, ...}) => (name, comment, int_only));
fun print_outer_syntax () =
let
fun pretty_cmd (name, comment, _) =
Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
- val (int_cmds, cmds) = List.partition #3 (dest_parsers ());
+ val (int_cmds, cmds) = List.partition #3 (dest_commands ());
in
[Pretty.strs ("syntax keywords:" :: map quote (OuterKeyword.dest_keywords ())),
Pretty.big_list "commands:" (map pretty_cmd cmds),
@@ -194,7 +199,7 @@
Source.of_string str
|> Symbol.source {do_recover = false}
|> T.source {do_recover = SOME false} OuterKeyword.get_lexicons pos
- |> toplevel_source false NONE get_parser
+ |> toplevel_source false NONE get_command
|> Source.exhaust;
@@ -225,39 +230,39 @@
Source.tty
|> Symbol.source {do_recover = true}
|> T.source {do_recover = SOME true} OuterKeyword.get_lexicons Position.none
- |> toplevel_source term (SOME true) get_parser;
+ |> toplevel_source term (SOME true) get_command;
(* prepare toplevel commands -- fail-safe *)
val not_singleton = "Exactly one command expected";
-fun prepare_span parser span =
+fun prepare_span commands span =
let
- val range_pos = Position.encode_range (ThyEdit.span_range span);
- val toks = ThyEdit.span_content span;
- val _ = List.app ThyEdit.report_token toks;
+ val range_pos = Position.encode_range (ThySyntax.span_range span);
+ val toks = ThySyntax.span_content span;
+ val _ = List.app ThySyntax.report_token toks;
in
- (case Source.exhaust (toplevel_source false NONE (K parser) (Source.of_list toks)) of
+ (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
[tr] => (tr, true)
| [] => (Toplevel.ignored range_pos, false)
| _ => (Toplevel.malformed range_pos not_singleton, true))
handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
-fun prepare_unit parser (cmd, proof, proper_proof) =
+fun prepare_unit commands (cmd, proof, proper_proof) =
let
- val (tr, proper_cmd) = prepare_span parser cmd;
- val proof_trs = map (prepare_span parser) proof |> filter #2 |> map #1;
+ val (tr, proper_cmd) = prepare_span commands cmd;
+ val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
in
if proper_cmd andalso proper_proof then [(tr, proof_trs)]
else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
end;
fun prepare_command pos str =
- let val (lexs, parser) = get_syntax () in
- (case ThyEdit.parse_spans lexs pos str of
- [span] => #1 (prepare_span parser span)
+ let val (lexs, commands) = get_syntax () in
+ (case ThySyntax.parse_spans lexs pos str of
+ [span] => #1 (prepare_span commands span)
| _ => Toplevel.malformed pos not_singleton)
end;
@@ -266,18 +271,18 @@
fun load_thy name pos text time =
let
- val (lexs, parser) = get_syntax ();
+ val (lexs, commands) = get_syntax ();
val _ = Present.init_theory name;
- val toks = Source.exhausted (ThyEdit.token_source lexs pos (Source.of_list text));
- val spans = Source.exhaust (ThyEdit.span_source toks);
- val _ = List.app ThyEdit.report_span spans;
- val units = Source.exhaust (ThyEdit.unit_source (Source.of_list spans))
- |> maps (prepare_unit parser);
+ val toks = Source.exhausted (ThySyntax.token_source lexs pos (Source.of_list text));
+ val spans = Source.exhaust (ThySyntax.span_source toks);
+ val _ = List.app ThySyntax.report_span spans;
+ val units = Source.exhaust (ThySyntax.unit_source (Source.of_list spans))
+ |> maps (prepare_unit commands);
val _ = Present.theory_source name
- (fn () => HTML.html_mode (implode o map ThyEdit.present_span) spans);
+ (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
val _ = cond_timeit time "" (fn () =>
--- a/src/Pure/Isar/proof_context.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Jan 03 08:39:54 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/Isar/spec_parse.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML Sat Jan 03 08:39:54 2009 +0100
@@ -1,5 +1,4 @@
(* Title: Pure/Isar/spec_parse.ML
- ID: $Id$
Author: Makarius
Parsers for complex specifications.
@@ -7,35 +6,33 @@
signature SPEC_PARSE =
sig
- type token
- val attrib: OuterLex.token list -> Attrib.src * token list
- val attribs: token list -> Attrib.src list * token list
- val opt_attribs: token list -> Attrib.src list * token list
- val thm_name: string -> token list -> Attrib.binding * token list
- val opt_thm_name: string -> token list -> Attrib.binding * token list
- val spec: token list -> (Attrib.binding * string list) * token list
- val named_spec: token list -> (Attrib.binding * string list) * token list
- val spec_name: token list -> ((Binding.T * string) * Attrib.src list) * token list
- val spec_opt_name: token list -> ((Binding.T * string) * Attrib.src list) * token list
- val xthm: token list -> (Facts.ref * Attrib.src list) * token list
- val xthms1: token list -> (Facts.ref * Attrib.src list) list * token list
- val name_facts: token list ->
- (Attrib.binding * (Facts.ref * Attrib.src list) list) list * token list
- val locale_mixfix: token list -> mixfix * token list
- val locale_fixes: token list -> (Binding.T * string option * mixfix) list * token list
- val locale_insts: token list -> (string option list * (Attrib.binding * string) list) * token list
- val class_expr: token list -> string list * token list
- val locale_expr: token list -> Locale.expr * token list
- val locale_expression: OuterParse.token list -> Expression.expression * OuterParse.token list
- val locale_keyword: token list -> string * token list
- val context_element: token list -> Element.context * token list
- val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
- val general_statement: token list ->
- (Element.context list * Element.statement) * OuterLex.token list
- val statement_keyword: token list -> string * token list
- val specification: token list ->
- (Binding.T *
- ((Attrib.binding * string list) list * (Binding.T * string option) list)) list * token list
+ type token = OuterParse.token
+ type 'a parser = 'a OuterParse.parser
+ val attrib: Attrib.src parser
+ val attribs: Attrib.src list parser
+ val opt_attribs: Attrib.src list parser
+ val thm_name: string -> Attrib.binding parser
+ val opt_thm_name: string -> Attrib.binding parser
+ val spec: (Attrib.binding * string list) parser
+ val named_spec: (Attrib.binding * string list) parser
+ val spec_name: ((Binding.T * string) * Attrib.src list) parser
+ val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser
+ val xthm: (Facts.ref * Attrib.src list) parser
+ val xthms1: (Facts.ref * Attrib.src list) list parser
+ val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
+ val locale_mixfix: mixfix parser
+ val locale_fixes: (Binding.T * string option * mixfix) list parser
+ val locale_insts: (string option list * (Attrib.binding * string) list) parser
+ val class_expr: string list parser
+ val locale_expr: Locale.expr parser
+ val locale_expression: Expression.expression parser
+ val locale_keyword: string parser
+ val context_element: Element.context parser
+ val statement: (Attrib.binding * (string * string list) list) list parser
+ val general_statement: (Element.context list * Element.statement) parser
+ val statement_keyword: string parser
+ val specification:
+ (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser
end;
structure SpecParse: SPEC_PARSE =
@@ -43,6 +40,7 @@
structure P = OuterParse;
type token = P.token;
+type 'a parser = 'a P.parser;
(* theorem specifications *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/value_parse.ML Sat Jan 03 08:39:54 2009 +0100
@@ -0,0 +1,45 @@
+(* Title: Pure/Isar/value_parse.ML
+ Author: Makarius
+
+Outer syntax parsers for basic ML values.
+*)
+
+signature VALUE_PARSE =
+sig
+ type 'a parser = 'a OuterParse.parser
+ val comma: 'a parser -> 'a parser
+ val equal: 'a parser -> 'a parser
+ val parens: 'a parser -> 'a parser
+ val pair: 'a parser -> 'b parser -> ('a * 'b) parser
+ val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
+ val properties: Properties.T parser
+end;
+
+structure ValueParse: VALUE_PARSE =
+struct
+
+structure P = OuterParse;
+type 'a parser = 'a P.parser;
+
+
+(* syntax utilities *)
+
+fun comma p = P.$$$ "," |-- P.!!! p;
+fun equal p = P.$$$ "=" |-- P.!!! p;
+fun parens p = P.$$$ "(" |-- P.!!! (p --| P.$$$ ")");
+
+
+(* tuples *)
+
+val unit = parens (Scan.succeed ());
+fun pair p1 p2 = parens (p1 -- comma p2);
+fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> P.triple1;
+
+
+(* lists *)
+
+fun list p = parens (P.enum "," p);
+val properties = list (P.string -- equal P.string);
+
+end;
+
--- a/src/Pure/ProofGeneral/pgip_parser.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Sat Jan 03 08:39:54 2009 +0100
@@ -92,18 +92,18 @@
fun parse_span span =
let
- val kind = ThyEdit.span_kind span;
- val toks = ThyEdit.span_content span;
- val text = implode (map (PrintMode.setmp [] ThyEdit.present_token) toks);
+ val kind = ThySyntax.span_kind span;
+ val toks = ThySyntax.span_content span;
+ val text = implode (map (PrintMode.setmp [] ThySyntax.present_token) toks);
in
(case kind of
- ThyEdit.Command name => parse_command name text
- | ThyEdit.Ignored => [D.Whitespace {text = text}]
- | ThyEdit.Malformed => [D.Unparseable {text = text}])
+ ThySyntax.Command name => parse_command name text
+ | ThySyntax.Ignored => [D.Whitespace {text = text}]
+ | ThySyntax.Malformed => [D.Unparseable {text = text}])
end;
fun pgip_parser pos str =
- maps parse_span (ThyEdit.parse_spans (OuterKeyword.get_lexicons ()) pos str);
+ maps parse_span (ThySyntax.parse_spans (OuterKeyword.get_lexicons ()) pos str);
end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Syntax/lexicon.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Sat Jan 03 08:39:54 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 Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Thy/latex.ML Sat Jan 03 08:39:54 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_edit.ML Sat Jan 03 08:39:18 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,194 +0,0 @@
-(* Title: Pure/Thy/thy_edit.ML
- ID: $Id$
- Author: Makarius
-
-Basic editor operations on theory sources.
-*)
-
-signature THY_EDIT =
-sig
- val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
- (OuterLex.token, (SymbolPos.T, Position.T * (Symbol.symbol, (string, 'a)
- Source.source) Source.source) Source.source) Source.source
- val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
- val present_token: OuterLex.token -> output
- val report_token: OuterLex.token -> unit
- datatype span_kind = Command of string | Ignored | Malformed
- type span
- val span_kind: span -> span_kind
- val span_content: span -> OuterLex.token list
- val span_range: span -> Position.range
- val span_source: (OuterLex.token, 'a) Source.source ->
- (span, (OuterLex.token, 'a) Source.source) Source.source
- val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
- val present_span: span -> output
- val report_span: span -> unit
- val unit_source: (span, 'a) Source.source ->
- (span * span list * bool, (span, 'a) Source.source) Source.source
-end;
-
-structure ThyEdit: THY_EDIT =
-struct
-
-structure K = OuterKeyword;
-structure T = OuterLex;
-structure P = OuterParse;
-
-
-(** tokens **)
-
-(* parse *)
-
-fun token_source lexs pos src =
- Symbol.source {do_recover = true} src
- |> T.source {do_recover = SOME false} (K lexs) pos;
-
-fun parse_tokens lexs pos str =
- Source.of_string str
- |> token_source lexs pos
- |> Source.exhaust;
-
-
-(* present *)
-
-local
-
-val token_kind_markup =
- fn T.Command => (Markup.commandN, [])
- | T.Keyword => (Markup.keywordN, [])
- | 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.Nat => Markup.ident
- | T.String => Markup.string
- | T.AltString => Markup.altstring
- | T.Verbatim => Markup.verbatim
- | T.Space => Markup.none
- | T.Comment => Markup.comment
- | T.InternalValue => Markup.none
- | T.Malformed => Markup.malformed
- | T.Error _ => Markup.malformed
- | T.Sync => Markup.control
- | T.EOF => Markup.control;
-
-in
-
-fun present_token tok =
- Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
-
-fun report_token tok =
- Position.report (token_kind_markup (T.kind_of tok)) (T.position_of tok);
-
-end;
-
-
-
-(** spans **)
-
-(* type span *)
-
-datatype span_kind = Command of string | Ignored | Malformed;
-datatype span = Span of span_kind * OuterLex.token list;
-
-fun span_kind (Span (k, _)) = k;
-fun span_content (Span (_, toks)) = toks;
-
-fun span_range span =
- (case span_content span of
- [] => (Position.none, Position.none)
- | toks =>
- let
- val start_pos = T.position_of (hd toks);
- val end_pos = T.end_position_of (List.last toks);
- in (start_pos, end_pos) end);
-
-
-(* parse *)
-
-local
-
-val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
-
-val body = Scan.unless (Scan.many is_whitespace -- Scan.ahead (P.command || P.eof)) P.not_eof;
-
-val span =
- Scan.ahead P.command -- P.not_eof -- Scan.repeat body
- >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
- Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
- Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
-
-in
-
-fun span_source src = Source.source T.stopper (Scan.bulk span) NONE src;
-
-end;
-
-fun parse_spans lexs pos str =
- Source.of_string str
- |> token_source lexs pos
- |> span_source
- |> Source.exhaust;
-
-
-(* present *)
-
-local
-
-fun kind_markup (Command name) = Markup.command_span name
- | kind_markup Ignored = Markup.ignored_span
- | kind_markup Malformed = Markup.malformed_span;
-
-in
-
-fun present_span span =
- Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
-
-fun report_span span =
- Position.report (kind_markup (span_kind span)) (Position.encode_range (span_range span));
-
-end;
-
-
-
-(** units: commands with proof **)
-
-(* scanning spans *)
-
-val eof = Span (Command "", []);
-
-fun is_eof (Span (Command "", _)) = true
- | is_eof _ = false;
-
-val not_eof = not o is_eof;
-
-val stopper = Scan.stopper (K eof) is_eof;
-
-
-(* unit_source *)
-
-local
-
-fun command_with pred = Scan.one (fn (Span (Command name, _)) => pred name | _ => false);
-
-val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
- if d <= 0 then Scan.fail
- else
- command_with K.is_qed_global >> pair ~1 ||
- command_with K.is_proof_goal >> pair (d + 1) ||
- (if d = 0 then Scan.fail else command_with K.is_qed >> pair (d - 1)) ||
- Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
-
-val unit =
- command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
- Scan.one not_eof >> (fn a => (a, [], true));
-
-in
-
-fun unit_source src = Source.source stopper (Scan.bulk unit) NONE src;
-
-end;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_syntax.ML Sat Jan 03 08:39:54 2009 +0100
@@ -0,0 +1,193 @@
+(* Title: Pure/Thy/thy_syntax.ML
+ Author: Makarius
+
+Superficial theory syntax: tokens and spans.
+*)
+
+signature THY_SYNTAX =
+sig
+ val token_source: Scan.lexicon * Scan.lexicon -> Position.T -> (string, 'a) Source.source ->
+ (OuterLex.token, (SymbolPos.T, Position.T * (Symbol.symbol, (string, 'a)
+ Source.source) Source.source) Source.source) Source.source
+ val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> OuterLex.token list
+ val present_token: OuterLex.token -> output
+ val report_token: OuterLex.token -> unit
+ datatype span_kind = Command of string | Ignored | Malformed
+ type span
+ val span_kind: span -> span_kind
+ val span_content: span -> OuterLex.token list
+ val span_range: span -> Position.range
+ val span_source: (OuterLex.token, 'a) Source.source ->
+ (span, (OuterLex.token, 'a) Source.source) Source.source
+ val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
+ val present_span: span -> output
+ val report_span: span -> unit
+ val unit_source: (span, 'a) Source.source ->
+ (span * span list * bool, (span, 'a) Source.source) Source.source
+end;
+
+structure ThySyntax: THY_SYNTAX =
+struct
+
+structure K = OuterKeyword;
+structure T = OuterLex;
+structure P = OuterParse;
+
+
+(** tokens **)
+
+(* parse *)
+
+fun token_source lexs pos src =
+ Symbol.source {do_recover = true} src
+ |> T.source {do_recover = SOME false} (K lexs) pos;
+
+fun parse_tokens lexs pos str =
+ Source.of_string str
+ |> token_source lexs pos
+ |> Source.exhaust;
+
+
+(* present *)
+
+local
+
+val token_kind_markup =
+ fn T.Command => (Markup.commandN, [])
+ | T.Keyword => (Markup.keywordN, [])
+ | T.Ident => Markup.ident
+ | T.LongIdent => Markup.ident
+ | T.SymIdent => 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
+ | T.Verbatim => Markup.verbatim
+ | T.Space => Markup.none
+ | T.Comment => Markup.comment
+ | T.InternalValue => Markup.none
+ | T.Malformed => Markup.malformed
+ | T.Error _ => Markup.malformed
+ | T.Sync => Markup.control
+ | T.EOF => Markup.control;
+
+in
+
+fun present_token tok =
+ Markup.enclose (token_kind_markup (T.kind_of tok)) (Output.output (T.unparse tok));
+
+fun report_token tok =
+ Position.report (token_kind_markup (T.kind_of tok)) (T.position_of tok);
+
+end;
+
+
+
+(** spans **)
+
+(* type span *)
+
+datatype span_kind = Command of string | Ignored | Malformed;
+datatype span = Span of span_kind * OuterLex.token list;
+
+fun span_kind (Span (k, _)) = k;
+fun span_content (Span (_, toks)) = toks;
+
+fun span_range span =
+ (case span_content span of
+ [] => (Position.none, Position.none)
+ | toks =>
+ let
+ val start_pos = T.position_of (hd toks);
+ val end_pos = T.end_position_of (List.last toks);
+ in (start_pos, end_pos) end);
+
+
+(* parse *)
+
+local
+
+val is_whitespace = T.is_kind T.Space orf T.is_kind T.Comment;
+
+val body = Scan.unless (Scan.many is_whitespace -- Scan.ahead (P.command || P.eof)) P.not_eof;
+
+val span =
+ Scan.ahead P.command -- P.not_eof -- Scan.repeat body
+ >> (fn ((name, c), bs) => Span (Command name, c :: bs)) ||
+ Scan.many1 is_whitespace >> (fn toks => Span (Ignored, toks)) ||
+ Scan.repeat1 body >> (fn toks => Span (Malformed, toks));
+
+in
+
+fun span_source src = Source.source T.stopper (Scan.bulk span) NONE src;
+
+end;
+
+fun parse_spans lexs pos str =
+ Source.of_string str
+ |> token_source lexs pos
+ |> span_source
+ |> Source.exhaust;
+
+
+(* present *)
+
+local
+
+fun kind_markup (Command name) = Markup.command_span name
+ | kind_markup Ignored = Markup.ignored_span
+ | kind_markup Malformed = Markup.malformed_span;
+
+in
+
+fun present_span span =
+ Markup.enclose (kind_markup (span_kind span)) (implode (map present_token (span_content span)));
+
+fun report_span span =
+ Position.report (kind_markup (span_kind span)) (Position.encode_range (span_range span));
+
+end;
+
+
+
+(** units: commands with proof **)
+
+(* scanning spans *)
+
+val eof = Span (Command "", []);
+
+fun is_eof (Span (Command "", _)) = true
+ | is_eof _ = false;
+
+val not_eof = not o is_eof;
+
+val stopper = Scan.stopper (K eof) is_eof;
+
+
+(* unit_source *)
+
+local
+
+fun command_with pred = Scan.one (fn (Span (Command name, _)) => pred name | _ => false);
+
+val proof = Scan.pass 1 (Scan.repeat (Scan.depend (fn d =>
+ if d <= 0 then Scan.fail
+ else
+ command_with K.is_qed_global >> pair ~1 ||
+ command_with K.is_proof_goal >> pair (d + 1) ||
+ (if d = 0 then Scan.fail else command_with K.is_qed >> pair (d - 1)) ||
+ Scan.unless (command_with K.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
+
+val unit =
+ command_with K.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
+ Scan.one not_eof >> (fn a => (a, [], true));
+
+in
+
+fun unit_source src = Source.source stopper (Scan.bulk unit) NONE src;
+
+end;
+
+end;
--- a/src/Pure/Tools/isabelle_process.ML Sat Jan 03 08:39:18 2009 +0100
+++ b/src/Pure/Tools/isabelle_process.ML Sat Jan 03 08:39:54 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;