# HG changeset patch # User wenzelm # Date 1116346231 -7200 # Node ID c81578ac2d31ec6ef74a7a8caf2cabe23c641722 # Parent f044579b147c9e23ba03769016e5a23ef5c0fda7 tuned; diff -r f044579b147c -r c81578ac2d31 NEWS --- 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 @@ \ 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 \. - -* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}" - (and similarly for "\" instead of ":") + Similarly for all quantifiers: "ALL x > y" etc. The x-symbol for >= + is \. + +* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}" (and similarly for + "\" instead of ":"). * HOL/SetInterval: The syntax for open intervals has changed: diff -r f044579b147c -r c81578ac2d31 src/Pure/General/symbol.ML --- 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; diff -r f044579b147c -r c81578ac2d31 src/Pure/Isar/constdefs.ML --- 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; - diff -r f044579b147c -r c81578ac2d31 src/Pure/Isar/isar_cmd.ML --- 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; - diff -r f044579b147c -r c81578ac2d31 src/Pure/Isar/isar_syn.ML --- 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; - diff -r f044579b147c -r c81578ac2d31 src/Pure/Isar/isar_thy.ML --- 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; - diff -r f044579b147c -r c81578ac2d31 src/Pure/Isar/outer_parse.ML --- 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; - diff -r f044579b147c -r c81578ac2d31 src/Pure/Isar/proof.ML --- 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; - diff -r f044579b147c -r c81578ac2d31 src/Pure/Isar/proof_context.ML --- 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; - diff -r f044579b147c -r c81578ac2d31 src/Pure/Isar/session.ML --- 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); diff -r f044579b147c -r c81578ac2d31 src/Pure/Syntax/parser.ML --- 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;