--- a/NEWS Tue May 17 18:10:31 2005 +0200
+++ b/NEWS Tue May 17 18:10:31 2005 +0200
@@ -86,8 +86,8 @@
* Pure: tuned internal renaming of symbolic identifiers -- attach
primes instead of base 26 numbers.
-* Pure: new flag show_var_qmarks to control printing of leading
- question marks of variable names.
+* Pure: new flag show_question_marks controls printing of leading
+ question marks in schematic variable names.
* Pure: new version of thms_containing that searches for a list
of patterns instead of a list of constants. Available in
@@ -169,21 +169,23 @@
*** Document preparation ***
-* New antiquotation @{term_type term} printing a term with its
- type annotated
-
-* New antiquotation @{typeof term} printing the - surprise - the type of
- a term
-
-* New antiquotation @{const const} which is the same as @{term const} except
- that const must be a defined constant identifier; helpful for early detection
- of typoes
-
-* Two new antiquotations @{term_style style term} and @{thm_style style thm}
- which print a term / theorem applying a "style" to it; predefined styles
- are "lhs" and "rhs" printing the lhs/rhs of definitions, equations,
- inequations etc. and "conclusion" printing only the conclusion of a theorem.
- More styles may be defined using ML; see the "LaTeX Sugar" document for more
+* Several new antiquotation:
+
+ @{term_type term} prints a term with its type annotated;
+
+ @{typeof term} prints the type of a term;
+
+ @{const const} is the same as @{term const}, but checks
+ that the argument is a known logical constant;
+
+ @{term_style style term} and @{thm_style style thm} print a term or
+ theorem applying a "style" to it
+
+ Predefined styles are "lhs" and "rhs" printing the lhs/rhs of
+ definitions, equations, inequations etc. and "conclusion" printing
+ only the conclusion of a meta-logical statement theorem. Styles may
+ be defined via TermStyle.add_style in ML. See the "LaTeX Sugar"
+ document for more information.
* Antiquotations now provide the option 'locale=NAME' to specify an
alternative context used for evaluating and printing the subsequent
@@ -242,11 +244,11 @@
\<epsilon> becomes available as variable, constant etc.
* HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
- Similarly for all quantifiers: "ALL x > y" etc.
- The x-symbol for >= is \<ge>.
-
-* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}"
- (and similarly for "\<in>" instead of ":")
+ Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >=
+ is \<ge>.
+
+* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}" (and similarly for
+ "\<in>" instead of ":").
* HOL/SetInterval: The syntax for open intervals has changed:
--- a/src/Pure/General/symbol.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/General/symbol.ML Tue May 17 18:10:31 2005 +0200
@@ -439,8 +439,8 @@
(* bump string -- treat as base 26 or base 1 numbers *)
-fun symbolic_end (_ :: "\\<^isup>" :: _) = true
- | symbolic_end (_ :: "\\<^isub>" :: _) = true
+fun symbolic_end (_ :: "\\<^isub>" :: _) = true
+ | symbolic_end (_ :: "\\<^isup>" :: _) = true
| symbolic_end (s :: _) = is_symbolic s
| symbolic_end [] = false;
--- a/src/Pure/Isar/constdefs.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Isar/constdefs.ML Tue May 17 18:10:31 2005 +0200
@@ -83,4 +83,3 @@
ProofContext.cert_typ ProofContext.cert_term (K I);
end;
-
--- a/src/Pure/Isar/isar_cmd.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue May 17 18:10:31 2005 +0200
@@ -377,4 +377,3 @@
end;
end;
-
--- a/src/Pure/Isar/isar_syn.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML Tue May 17 18:10:31 2005 +0200
@@ -858,4 +858,3 @@
OuterSyntax.add_keywords IsarSyn.keywords;
OuterSyntax.add_parsers IsarSyn.parsers;
IsarOutput.add_hidden_commands IsarSyn.hidden_commands;
-
--- a/src/Pure/Isar/isar_thy.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML Tue May 17 18:10:31 2005 +0200
@@ -685,4 +685,3 @@
val context = init_context (ThyInfo.quiet_update_thy true);
end;
-
--- a/src/Pure/Isar/outer_parse.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Isar/outer_parse.ML Tue May 17 18:10:31 2005 +0200
@@ -365,4 +365,3 @@
end;
-
--- a/src/Pure/Isar/proof.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Isar/proof.ML Tue May 17 18:10:31 2005 +0200
@@ -976,4 +976,3 @@
structure BasicProof: BASIC_PROOF = Proof;
open BasicProof;
-
--- a/src/Pure/Isar/proof_context.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue May 17 18:10:31 2005 +0200
@@ -1639,4 +1639,3 @@
end;
end;
-
--- a/src/Pure/Isar/session.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Isar/session.ML Tue May 17 18:10:31 2005 +0200
@@ -20,19 +20,17 @@
(* session state *)
-val pure = "Pure";
-
-val session = ref ([pure]: string list);
+val session = ref ([Sign.PureN]: string list);
val session_path = ref ([]: string list);
val session_finished = ref false;
-val rpath = ref (NONE: Url.T option);
+val remote_path = ref (NONE: Url.T option);
(* access path *)
fun path () = ! session_path;
-fun str_of [] = pure
+fun str_of [] = Sign.PureN
| str_of elems = space_implode "/" elems;
fun name () = "Isabelle/" ^ str_of (path ());
@@ -67,25 +65,21 @@
(* use_dir *)
-(*
-val root_file = ThyLoad.ml_path "ROOT";
-*)
-
fun get_rpath rpath_str =
(if rpath_str = "" then () else
- if is_some (! rpath) then
+ if is_some (! remote_path) then
error "Path for remote theory browsing information may only be set once"
else
- rpath := SOME (Url.unpack rpath_str);
- (!rpath, rpath_str <> ""));
+ remote_path := SOME (Url.unpack rpath_str);
+ (! remote_path, rpath_str <> ""));
-fun use_dir root_file build modes reset info doc doc_graph parent name dump rpath_str level verbose hide =
+fun use_dir root build modes reset info doc doc_graph parent name dump rpath_str level verbose hide =
Library.setmp print_mode (modes @ ! print_mode)
(Library.setmp Proofterm.proofs level (Library.setmp IsarOutput.hide_commands hide (fn () =>
(init reset parent name;
Present.init build info doc doc_graph (path ()) name
(if dump = "" then NONE else SOME (Path.unpack dump)) (get_rpath rpath_str) verbose;
- File.use (Path.basic root_file);
+ File.use (Path.basic root);
finish ())))) ()
handle exn => (writeln (Toplevel.exn_message exn); exit 1);
--- a/src/Pure/Syntax/parser.ML Tue May 17 18:10:31 2005 +0200
+++ b/src/Pure/Syntax/parser.ML Tue May 17 18:10:31 2005 +0200
@@ -2,7 +2,7 @@
ID: $Id$
Author: Carsten Clasohm, Sonia Mahjoub, and Markus Wenzel, TU Muenchen
-Isabelle's main parser (used for terms and types).
+General context-free parser for the inner syntax of terms, types, etc.
*)
signature PARSER =
@@ -85,7 +85,7 @@
val (added_starts, lambdas') =
if is_none new_chain then ([], lambdas) else
let (*lookahead of chain's source*)
- val ((from_nts, from_tks), _) = Array.sub (prods, valOf new_chain);
+ val ((from_nts, from_tks), _) = Array.sub (prods, the new_chain);
(*copy from's lookahead to chain's destinations*)
fun copy_lookahead [] added = added
@@ -149,7 +149,7 @@
let
val new_lambda = is_none tk andalso nts subset lambdas;
- val new_tks = (if isSome tk then [valOf tk] else []) @
+ val new_tks = (if is_some tk then [the tk] else []) @
Library.foldl token_union ([], map starts_for_nt nts) \\
l_starts;
@@ -228,14 +228,14 @@
(*insert production into grammar*)
val (added_starts', prod_count') =
- if isSome chain_from then (added_starts', prod_count) (*don't store chain production*)
+ if is_some chain_from then (added_starts', prod_count) (*don't store chain production*)
else let
(*lookahead tokens of new production and on which
NTs lookahead depends*)
val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
val start_tks = Library.foldl token_union
- (if isSome start_tk then [valOf start_tk] else [],
+ (if is_some start_tk then [the start_tk] else [],
map starts_for_nt start_nts);
val opt_starts = (if new_lambda then [NONE]
@@ -261,7 +261,7 @@
(*store new production*)
fun store [] prods is_new =
- (prods, if isSome prod_count andalso is_new then
+ (prods, if is_some prod_count andalso is_new then
Option.map (fn x => x+1) prod_count
else prod_count, is_new)
| store (tk :: tks) prods is_new =
@@ -270,7 +270,7 @@
(*if prod_count = NONE then we can assume that
grammar does not contain new production already*)
val (tk_prods', is_new') =
- if isSome prod_count then
+ if is_some prod_count then
if new_prod mem tk_prods then (tk_prods, false)
else (new_prod :: tk_prods, true)
else (new_prod :: tk_prods, true);
@@ -324,8 +324,8 @@
(*test if production could already be associated with
a member of new_tks*)
val lambda = length depends > 1 orelse
- not (null depends) andalso isSome tk
- andalso valOf tk mem new_tks;
+ not (null depends) andalso is_some tk
+ andalso the tk mem new_tks;
(*associate production with new starting tokens*)
fun copy [] nt_prods = nt_prods
@@ -395,7 +395,7 @@
fun pretty_symb (Terminal (Token s)) = Pretty.quote (Pretty.str s)
| pretty_symb (Terminal tok) = Pretty.str (str_of_token tok)
| pretty_symb (Nonterminal (tag, p)) =
- let val name = fst (valOf (find_first (fn (n, t) => t = tag) taglist));
+ let val name = fst (the (find_first (fn (n, t) => t = tag) taglist));
in Pretty.str (name ^ "[" ^ string_of_int p ^ "]") end;
fun pretty_const "" = []
@@ -535,7 +535,7 @@
| store_tag nt_count tags tag =
let val (nt_count', tags', tag') =
get_tag nt_count tags
- (fst (valOf (find_first (fn (n, t) => t = tag) tag_list)));
+ (fst (the (find_first (fn (n, t) => t = tag) tag_list)));
in Array.update (table, tag, tag');
store_tag nt_count' tags' (tag-1)
end;
@@ -695,11 +695,11 @@
(*get all productions of a NT and NTs chained to it which can
be started by specified token*)
fun prods_for prods chains include_none tk nts =
-let (*similar to token_assoc but does not automatically include 'NONE' key*)
- fun token_assoc2 (list, key) =
+let
+ fun token_assoc (list, key) =
let fun assoc [] result = result
| assoc ((keyi, pi) :: pairs) result =
- if isSome keyi andalso matching_tokens (valOf keyi, key)
+ if is_some keyi andalso matching_tokens (the keyi, key)
orelse include_none andalso is_none keyi then
assoc pairs (pi @ result)
else assoc pairs result;
@@ -708,7 +708,7 @@
fun get_prods [] result = result
| get_prods (nt :: nts) result =
let val nt_prods = snd (Array.sub (prods, nt));
- in get_prods nts ((token_assoc2 (nt_prods, tk)) @ result) end;
+ in get_prods nts ((token_assoc (nt_prods, tk)) @ result) end;
in get_prods (connected_with chains nts nts) [] end;