tuned;
authorwenzelm
Tue May 17 18:10:31 2005 +0200 (2005-05-17 ago)
changeset 15979c81578ac2d31
parent 15978 f044579b147c
child 15980 3dfcdb19f242
tuned;
NEWS
src/Pure/General/symbol.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/session.ML
src/Pure/Syntax/parser.ML
     1.1 --- a/NEWS	Tue May 17 18:10:31 2005 +0200
     1.2 +++ b/NEWS	Tue May 17 18:10:31 2005 +0200
     1.3 @@ -86,8 +86,8 @@
     1.4  * Pure: tuned internal renaming of symbolic identifiers -- attach
     1.5    primes instead of base 26 numbers.
     1.6  
     1.7 -* Pure: new flag show_var_qmarks to control printing of leading
     1.8 -  question marks of variable names.
     1.9 +* Pure: new flag show_question_marks controls printing of leading
    1.10 +  question marks in schematic variable names.
    1.11  
    1.12  * Pure: new version of thms_containing that searches for a list 
    1.13    of patterns instead of a list of constants. Available in 
    1.14 @@ -169,21 +169,23 @@
    1.15  
    1.16  *** Document preparation ***
    1.17  
    1.18 -* New antiquotation @{term_type term} printing a term with its
    1.19 -  type annotated
    1.20 -
    1.21 -* New antiquotation @{typeof term} printing the - surprise - the type of 
    1.22 -  a term
    1.23 -
    1.24 -* New antiquotation @{const const} which is the same as @{term const} except
    1.25 -  that const must be a defined constant identifier; helpful for early detection
    1.26 -  of typoes
    1.27 -
    1.28 -* Two new antiquotations @{term_style style term} and @{thm_style style thm}
    1.29 -  which print a term / theorem applying a "style" to it; predefined styles
    1.30 -  are "lhs" and "rhs" printing the lhs/rhs of definitions, equations,
    1.31 -  inequations etc. and "conclusion" printing only the conclusion of a theorem.
    1.32 -  More styles may be defined using ML; see the "LaTeX Sugar" document for more
    1.33 +* Several new antiquotation:
    1.34 +
    1.35 +  @{term_type term} prints a term with its type annotated;
    1.36 +
    1.37 +  @{typeof term} prints the type of a term;
    1.38 +
    1.39 +  @{const const} is the same as @{term const}, but checks
    1.40 +    that the argument is a known logical constant;
    1.41 +
    1.42 +  @{term_style style term} and @{thm_style style thm} print a term or
    1.43 +    theorem applying a "style" to it
    1.44 +
    1.45 +  Predefined styles are "lhs" and "rhs" printing the lhs/rhs of
    1.46 +  definitions, equations, inequations etc. and "conclusion" printing
    1.47 +  only the conclusion of a meta-logical statement theorem.  Styles may
    1.48 +  be defined via TermStyle.add_style in ML.  See the "LaTeX Sugar"
    1.49 +  document for more information.
    1.50  
    1.51  * Antiquotations now provide the option 'locale=NAME' to specify an
    1.52    alternative context used for evaluating and printing the subsequent
    1.53 @@ -242,11 +244,11 @@
    1.54    \<epsilon> becomes available as variable, constant etc.
    1.55  
    1.56  * HOL: "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
    1.57 -  Similarly for all quantifiers: "ALL x > y" etc.
    1.58 -  The x-symbol for >= is \<ge>.
    1.59 -
    1.60 -* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}"
    1.61 -           (and similarly for "\<in>" instead of ":")
    1.62 +  Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
    1.63 +  is \<ge>.
    1.64 +
    1.65 +* HOL/Set: "{x:A. P}" abbreviates "{x. x:A & P}" (and similarly for
    1.66 +  "\<in>" instead of ":").
    1.67  
    1.68  * HOL/SetInterval: The syntax for open intervals has changed:
    1.69  
     2.1 --- a/src/Pure/General/symbol.ML	Tue May 17 18:10:31 2005 +0200
     2.2 +++ b/src/Pure/General/symbol.ML	Tue May 17 18:10:31 2005 +0200
     2.3 @@ -439,8 +439,8 @@
     2.4  
     2.5  (* bump string -- treat as base 26 or base 1 numbers *)
     2.6  
     2.7 -fun symbolic_end (_ :: "\\<^isup>" :: _) = true
     2.8 -  | symbolic_end (_ :: "\\<^isub>" :: _) = true
     2.9 +fun symbolic_end (_ :: "\\<^isub>" :: _) = true
    2.10 +  | symbolic_end (_ :: "\\<^isup>" :: _) = true
    2.11    | symbolic_end (s :: _) = is_symbolic s
    2.12    | symbolic_end [] = false;
    2.13  
     3.1 --- a/src/Pure/Isar/constdefs.ML	Tue May 17 18:10:31 2005 +0200
     3.2 +++ b/src/Pure/Isar/constdefs.ML	Tue May 17 18:10:31 2005 +0200
     3.3 @@ -83,4 +83,3 @@
     3.4    ProofContext.cert_typ ProofContext.cert_term (K I);
     3.5  
     3.6  end;
     3.7 -
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue May 17 18:10:31 2005 +0200
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue May 17 18:10:31 2005 +0200
     4.3 @@ -377,4 +377,3 @@
     4.4  end;
     4.5  
     4.6  end;
     4.7 -
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Tue May 17 18:10:31 2005 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue May 17 18:10:31 2005 +0200
     5.3 @@ -858,4 +858,3 @@
     5.4  OuterSyntax.add_keywords IsarSyn.keywords;
     5.5  OuterSyntax.add_parsers IsarSyn.parsers;
     5.6  IsarOutput.add_hidden_commands IsarSyn.hidden_commands;
     5.7 -
     6.1 --- a/src/Pure/Isar/isar_thy.ML	Tue May 17 18:10:31 2005 +0200
     6.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue May 17 18:10:31 2005 +0200
     6.3 @@ -685,4 +685,3 @@
     6.4  val context = init_context (ThyInfo.quiet_update_thy true);
     6.5  
     6.6  end;
     6.7 -
     7.1 --- a/src/Pure/Isar/outer_parse.ML	Tue May 17 18:10:31 2005 +0200
     7.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue May 17 18:10:31 2005 +0200
     7.3 @@ -365,4 +365,3 @@
     7.4  
     7.5  
     7.6  end;
     7.7 -
     8.1 --- a/src/Pure/Isar/proof.ML	Tue May 17 18:10:31 2005 +0200
     8.2 +++ b/src/Pure/Isar/proof.ML	Tue May 17 18:10:31 2005 +0200
     8.3 @@ -976,4 +976,3 @@
     8.4  
     8.5  structure BasicProof: BASIC_PROOF = Proof;
     8.6  open BasicProof;
     8.7 -
     9.1 --- a/src/Pure/Isar/proof_context.ML	Tue May 17 18:10:31 2005 +0200
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Tue May 17 18:10:31 2005 +0200
     9.3 @@ -1639,4 +1639,3 @@
     9.4    end;
     9.5  
     9.6  end;
     9.7 -
    10.1 --- a/src/Pure/Isar/session.ML	Tue May 17 18:10:31 2005 +0200
    10.2 +++ b/src/Pure/Isar/session.ML	Tue May 17 18:10:31 2005 +0200
    10.3 @@ -20,19 +20,17 @@
    10.4  
    10.5  (* session state *)
    10.6  
    10.7 -val pure = "Pure";
    10.8 -
    10.9 -val session = ref ([pure]: string list);
   10.10 +val session = ref ([Sign.PureN]: string list);
   10.11  val session_path = ref ([]: string list);
   10.12  val session_finished = ref false;
   10.13 -val rpath = ref (NONE: Url.T option);
   10.14 +val remote_path = ref (NONE: Url.T option);
   10.15  
   10.16  
   10.17  (* access path *)
   10.18  
   10.19  fun path () = ! session_path;
   10.20  
   10.21 -fun str_of [] = pure
   10.22 +fun str_of [] = Sign.PureN
   10.23    | str_of elems = space_implode "/" elems;
   10.24  
   10.25  fun name () = "Isabelle/" ^ str_of (path ());
   10.26 @@ -67,25 +65,21 @@
   10.27  
   10.28  (* use_dir *)
   10.29  
   10.30 -(*
   10.31 -val root_file = ThyLoad.ml_path "ROOT";
   10.32 -*)
   10.33 -
   10.34  fun get_rpath rpath_str =
   10.35    (if rpath_str = "" then () else
   10.36 -     if is_some (! rpath) then
   10.37 +     if is_some (! remote_path) then
   10.38         error "Path for remote theory browsing information may only be set once"
   10.39       else
   10.40 -       rpath := SOME (Url.unpack rpath_str);
   10.41 -   (!rpath, rpath_str <> ""));
   10.42 +       remote_path := SOME (Url.unpack rpath_str);
   10.43 +   (! remote_path, rpath_str <> ""));
   10.44  
   10.45 -fun use_dir root_file build modes reset info doc doc_graph parent name dump rpath_str level verbose hide =
   10.46 +fun use_dir root build modes reset info doc doc_graph parent name dump rpath_str level verbose hide =
   10.47    Library.setmp print_mode (modes @ ! print_mode)
   10.48      (Library.setmp Proofterm.proofs level (Library.setmp IsarOutput.hide_commands hide (fn () =>
   10.49        (init reset parent name;
   10.50         Present.init build info doc doc_graph (path ()) name
   10.51           (if dump = "" then NONE else SOME (Path.unpack dump)) (get_rpath rpath_str) verbose;
   10.52 -       File.use (Path.basic root_file);
   10.53 +       File.use (Path.basic root);
   10.54         finish ())))) ()
   10.55    handle exn => (writeln (Toplevel.exn_message exn); exit 1);
   10.56  
    11.1 --- a/src/Pure/Syntax/parser.ML	Tue May 17 18:10:31 2005 +0200
    11.2 +++ b/src/Pure/Syntax/parser.ML	Tue May 17 18:10:31 2005 +0200
    11.3 @@ -2,7 +2,7 @@
    11.4      ID:         $Id$
    11.5      Author:     Carsten Clasohm, Sonia Mahjoub, and Markus Wenzel, TU Muenchen
    11.6  
    11.7 -Isabelle's main parser (used for terms and types).
    11.8 +General context-free parser for the inner syntax of terms, types, etc.
    11.9  *)
   11.10  
   11.11  signature PARSER =
   11.12 @@ -85,7 +85,7 @@
   11.13        val (added_starts, lambdas') =
   11.14          if is_none new_chain then ([], lambdas) else
   11.15          let (*lookahead of chain's source*)
   11.16 -            val ((from_nts, from_tks), _) = Array.sub (prods, valOf new_chain);
   11.17 +            val ((from_nts, from_tks), _) = Array.sub (prods, the new_chain);
   11.18  
   11.19              (*copy from's lookahead to chain's destinations*)
   11.20              fun copy_lookahead [] added = added
   11.21 @@ -149,7 +149,7 @@
   11.22                        let
   11.23                          val new_lambda = is_none tk andalso nts subset lambdas;
   11.24  
   11.25 -                        val new_tks = (if isSome tk then [valOf tk] else []) @
   11.26 +                        val new_tks = (if is_some tk then [the tk] else []) @
   11.27                            Library.foldl token_union ([], map starts_for_nt nts) \\
   11.28                            l_starts;
   11.29  
   11.30 @@ -228,14 +228,14 @@
   11.31  
   11.32        (*insert production into grammar*)
   11.33        val (added_starts', prod_count') =
   11.34 -        if isSome chain_from then (added_starts', prod_count)  (*don't store chain production*)
   11.35 +        if is_some chain_from then (added_starts', prod_count)  (*don't store chain production*)
   11.36          else let
   11.37            (*lookahead tokens of new production and on which
   11.38              NTs lookahead depends*)
   11.39            val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
   11.40  
   11.41            val start_tks = Library.foldl token_union
   11.42 -                          (if isSome start_tk then [valOf start_tk] else [],
   11.43 +                          (if is_some start_tk then [the start_tk] else [],
   11.44                             map starts_for_nt start_nts);
   11.45  
   11.46            val opt_starts = (if new_lambda then [NONE]
   11.47 @@ -261,7 +261,7 @@
   11.48  
   11.49                  (*store new production*)
   11.50                  fun store [] prods is_new =
   11.51 -                      (prods, if isSome prod_count andalso is_new then
   11.52 +                      (prods, if is_some prod_count andalso is_new then
   11.53                                  Option.map (fn x => x+1) prod_count
   11.54                                else prod_count, is_new)
   11.55                    | store (tk :: tks) prods is_new =
   11.56 @@ -270,7 +270,7 @@
   11.57                          (*if prod_count = NONE then we can assume that
   11.58                            grammar does not contain new production already*)
   11.59                          val (tk_prods', is_new') =
   11.60 -                          if isSome prod_count then
   11.61 +                          if is_some prod_count then
   11.62                              if new_prod mem tk_prods then (tk_prods, false)
   11.63                              else (new_prod :: tk_prods, true)
   11.64                            else (new_prod :: tk_prods, true);
   11.65 @@ -324,8 +324,8 @@
   11.66                        (*test if production could already be associated with
   11.67                          a member of new_tks*)
   11.68                        val lambda = length depends > 1 orelse
   11.69 -                                   not (null depends) andalso isSome tk
   11.70 -                                   andalso valOf tk mem new_tks;
   11.71 +                                   not (null depends) andalso is_some tk
   11.72 +                                   andalso the tk mem new_tks;
   11.73  
   11.74                        (*associate production with new starting tokens*)
   11.75                        fun copy [] nt_prods = nt_prods
   11.76 @@ -395,7 +395,7 @@
   11.77      fun pretty_symb (Terminal (Token s)) = Pretty.quote (Pretty.str s)
   11.78        | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok)
   11.79        | pretty_symb (Nonterminal (tag, p)) =
   11.80 -        let val name = fst (valOf (find_first (fn (n, t) => t = tag) taglist));
   11.81 +        let val name = fst (the (find_first (fn (n, t) => t = tag) taglist));
   11.82          in Pretty.str (name ^ "[" ^ string_of_int p ^ "]") end;
   11.83  
   11.84      fun pretty_const "" = []
   11.85 @@ -535,7 +535,7 @@
   11.86              | store_tag nt_count tags tag =
   11.87                let val (nt_count', tags', tag') =
   11.88                     get_tag nt_count tags
   11.89 -                     (fst (valOf (find_first (fn (n, t) => t = tag) tag_list)));
   11.90 +                     (fst (the (find_first (fn (n, t) => t = tag) tag_list)));
   11.91                in Array.update (table, tag, tag');
   11.92                   store_tag nt_count' tags' (tag-1)
   11.93                end;
   11.94 @@ -695,11 +695,11 @@
   11.95  (*get all productions of a NT and NTs chained to it which can
   11.96    be started by specified token*)
   11.97  fun prods_for prods chains include_none tk nts =
   11.98 -let (*similar to token_assoc but does not automatically include 'NONE' key*)
   11.99 -    fun token_assoc2 (list, key) =
  11.100 +let
  11.101 +    fun token_assoc (list, key) =
  11.102        let fun assoc [] result = result
  11.103              | assoc ((keyi, pi) :: pairs) result =
  11.104 -                if isSome keyi andalso matching_tokens (valOf keyi, key)
  11.105 +                if is_some keyi andalso matching_tokens (the keyi, key)
  11.106                     orelse include_none andalso is_none keyi then
  11.107                    assoc pairs (pi @ result)
  11.108                  else assoc pairs result;
  11.109 @@ -708,7 +708,7 @@
  11.110      fun get_prods [] result = result
  11.111        | get_prods (nt :: nts) result =
  11.112          let val nt_prods = snd (Array.sub (prods, nt));
  11.113 -        in get_prods nts ((token_assoc2 (nt_prods, tk)) @ result) end;
  11.114 +        in get_prods nts ((token_assoc (nt_prods, tk)) @ result) end;
  11.115  in get_prods (connected_with chains nts nts) [] end;
  11.116  
  11.117