--- a/NEWS Sat Dec 04 21:53:00 2010 +0100
+++ b/NEWS Sun Dec 05 08:34:02 2010 +0100
@@ -582,6 +582,12 @@
*** ML ***
+* Syntax.pretty_priority (default 0) configures the required priority
+of pretty-printed output and thus affects insertion of parentheses.
+
+* Syntax.default_root (default "any") configures the inner syntax
+category (nonterminal symbol) for parsing of terms.
+
* Former exception Library.UnequalLengths now coincides with
ListPair.UnequalLengths.
--- a/etc/isar-keywords-ZF.el Sat Dec 04 21:53:00 2010 +0100
+++ b/etc/isar-keywords-ZF.el Sun Dec 05 08:34:02 2010 +0100
@@ -107,6 +107,7 @@
"nonterminals"
"notation"
"note"
+ "notepad"
"obtain"
"oops"
"oracle"
@@ -383,6 +384,7 @@
"no_type_notation"
"nonterminals"
"notation"
+ "notepad"
"oracle"
"overloading"
"parse_ast_translation"
--- a/etc/isar-keywords.el Sat Dec 04 21:53:00 2010 +0100
+++ b/etc/isar-keywords.el Sun Dec 05 08:34:02 2010 +0100
@@ -144,6 +144,7 @@
"nonterminals"
"notation"
"note"
+ "notepad"
"obtain"
"oops"
"oracle"
@@ -489,6 +490,7 @@
"nominal_datatype"
"nonterminals"
"notation"
+ "notepad"
"oracle"
"overloading"
"parse_ast_translation"
--- a/src/HOL/Tools/Datatype/datatype_data.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Sun Dec 05 08:34:02 2010 +0100
@@ -242,23 +242,21 @@
val thy = ProofContext.theory_of ctxt;
val (vs, cos) = the_spec thy dtco;
val ty = Type (dtco, map TFree vs);
- fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
- Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
- | pretty_typ_bracket ty =
- Syntax.pretty_typ ctxt ty;
+ val pretty_typ_bracket =
+ Syntax.pretty_typ (Config.put Syntax.pretty_priority (Syntax.max_pri + 1) ctxt);
fun pretty_constr (co, tys) =
- (Pretty.block o Pretty.breaks)
+ Pretty.block (Pretty.breaks
(Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- map pretty_typ_bracket tys);
+ map pretty_typ_bracket tys));
val pretty_datatype =
Pretty.block
- (Pretty.command "datatype" :: Pretty.brk 1 ::
- Syntax.pretty_typ ctxt ty ::
- Pretty.str " =" :: Pretty.brk 1 ::
- flat (separate [Pretty.brk 1, Pretty.str "| "]
- (map (single o pretty_constr) cos)));
+ (Pretty.command "datatype" :: Pretty.brk 1 ::
+ Syntax.pretty_typ ctxt ty ::
+ Pretty.str " =" :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_constr) cos)));
in
- Thy_Output.output ctxt (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
+ Thy_Output.output ctxt
+ (Thy_Output.maybe_pretty_source (K (K pretty_datatype)) ctxt src [()])
end);
--- a/src/Pure/Isar/isar_syn.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Dec 05 08:34:02 2010 +0100
@@ -35,7 +35,8 @@
val _ =
Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
- (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
+ (Scan.succeed
+ (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
@@ -507,6 +508,11 @@
val _ = gen_theorem true Thm.corollaryK;
val _ =
+ Outer_Syntax.local_theory_to_proof "notepad"
+ "Isar proof state as formal notepad, without any result" Keyword.thy_decl
+ (Parse.begin >> K Proof.begin_notepad);
+
+val _ =
Outer_Syntax.local_theory_to_proof "example_proof"
"example proof body, without any result" Keyword.thy_schematic_goal
(Scan.succeed
--- a/src/Pure/Isar/proof.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Isar/proof.ML Sun Dec 05 08:34:02 2010 +0100
@@ -76,6 +76,8 @@
val begin_block: state -> state
val next_block: state -> state
val end_block: state -> state
+ val begin_notepad: Proof.context -> state
+ val end_notepad: state -> Proof.context
val proof: Method.text option -> state -> state Seq.seq
val defer: int option -> state -> state Seq.seq
val prefer: int -> state -> state Seq.seq
@@ -767,12 +769,30 @@
fun end_block state =
state
|> assert_forward
+ |> assert_bottom false
|> close_block
|> assert_current_goal false
|> close_block
|> export_facts state;
+(* global notepad *)
+
+val begin_notepad =
+ init
+ #> open_block
+ #> map_context (Variable.set_body true)
+ #> open_block;
+
+val end_notepad =
+ assert_forward
+ #> assert_bottom true
+ #> close_block
+ #> assert_current_goal false
+ #> close_block
+ #> context_of;
+
+
(* sub-proofs *)
fun proof opt_text =
--- a/src/Pure/Isar/proof_context.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Dec 05 08:34:02 2010 +0100
@@ -764,11 +764,19 @@
if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
val (syms, pos) = Syntax.parse_token ctxt markup text;
+ val default_root = Config.get ctxt Syntax.default_root;
+ val root =
+ (case T' of
+ Type (c, _) =>
+ if c <> "prop" andalso Type.is_logtype (tsig_of ctxt) c
+ then default_root else c
+ | _ => default_root);
+
fun check t = (Syntax.check_term ctxt (Type.constraint T' t); NONE)
handle ERROR msg => SOME msg;
val t =
Syntax.standard_parse_term check get_sort map_const map_free
- ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
+ ctxt (syn_of ctxt) root (syms, pos)
handle ERROR msg => parse_failed ctxt pos msg kind;
in t end;
--- a/src/Pure/Isar/token.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Isar/token.ML Sun Dec 05 08:34:02 2010 +0100
@@ -9,7 +9,7 @@
datatype kind =
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
- Malformed | Error of string | Sync | EOF
+ Error of string | Sync | EOF
datatype value =
Text of string | Typ of typ | Term of term | Fact of thm list |
Attribute of morphism -> attribute
@@ -90,7 +90,7 @@
datatype kind =
Command | Keyword | Ident | LongIdent | SymIdent | Var | TypeIdent | TypeVar |
Nat | Float | String | AltString | Verbatim | Space | Comment | InternalValue |
- Malformed | Error of string | Sync | EOF;
+ Error of string | Sync | EOF;
datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot;
@@ -111,7 +111,6 @@
| Space => "white space"
| Comment => "comment text"
| InternalValue => "internal value"
- | Malformed => "malformed symbolic character"
| Error _ => "bad input"
| Sync => "sync marker"
| EOF => "end-of-file";
@@ -331,7 +330,6 @@
scan_verbatim >> token_range Verbatim ||
scan_comment >> token_range Comment ||
scan_space >> token Space ||
- Scan.one (Symbol.is_malformed o Symbol_Pos.symbol) >> (token Malformed o single) ||
Scan.one (Symbol.is_sync o Symbol_Pos.symbol) >> (token Sync o single) ||
(Scan.max token_leq
(Scan.max token_leq
--- a/src/Pure/Isar/toplevel.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Isar/toplevel.ML Sun Dec 05 08:34:02 2010 +0100
@@ -486,12 +486,13 @@
let
val prf = init int gthy;
val skip = ! skip_proofs;
- val schematic = Proof.schematic_goal prf;
+ val (is_goal, no_skip) =
+ (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
in
- if skip andalso schematic then
+ if is_goal andalso skip andalso no_skip then
warning "Cannot skip proof of schematic goal statement"
else ();
- if skip andalso not schematic then
+ if skip andalso not no_skip then
SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
else Proof (Proof_Node.init prf, (finish gthy, gthy))
end
--- a/src/Pure/Syntax/parser.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Syntax/parser.ML Sun Dec 05 08:34:02 2010 +0100
@@ -841,7 +841,7 @@
val start_tag =
(case Symtab.lookup tags startsymbol of
SOME tag => tag
- | NONE => error ("Inner syntax: unknown startsymbol " ^ quote startsymbol));
+ | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol));
val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];
val s = length indata + 1;
val Estate = Array.array (s, []);
--- a/src/Pure/Syntax/printer.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Syntax/printer.ML Sun Dec 05 08:34:02 2010 +0100
@@ -22,6 +22,7 @@
val show_question_marks_default: bool Unsynchronized.ref
val show_question_marks_raw: Config.raw
val show_question_marks: bool Config.T
+ val pretty_priority: int Config.T
end;
signature PRINTER =
@@ -314,7 +315,9 @@
| is_chain [Arg _] = true
| is_chain _ = false;
-fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
+val pretty_priority = Config.int (Config.declare "Syntax.pretty_priority" (K (Config.Int 0)));
+
+fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 =
let
val {extern_class, extern_type, extern_const} = extern;
val show_brackets = Config.get ctxt show_brackets;
@@ -341,7 +344,9 @@
val (Ts, args') = synT markup (symbs, args);
in
if type_mode then (astT (t, p) @ Ts, args')
- else (pretty extern ctxt tabs trf tokentrf true curried t p @ Ts, args')
+ else
+ (pretty extern (Config.put pretty_priority p ctxt)
+ tabs trf tokentrf true curried t @ Ts, args')
end
| synT markup (String s :: symbs, args) =
let val (Ts, args') = synT markup (symbs, args);
@@ -414,21 +419,19 @@
| astT (Ast.Appl ((c as Ast.Constant a) :: (args as _ :: _)), p) = combT (c, a, args, p)
| astT (Ast.Appl (f :: (args as _ :: _)), p) = astT (appT (f, args), p)
| astT (ast as Ast.Appl _, _) = raise Ast.AST ("pretty: malformed ast", [ast]);
- in astT (ast0, p0) end;
+ in astT (ast0, Config.get ctxt pretty_priority) end;
(* pretty_term_ast *)
fun pretty_term_ast extern ctxt curried prtabs trf tokentrf ast =
- pretty extern ctxt (mode_tabs prtabs (print_mode_value ()))
- trf tokentrf false curried ast 0;
+ pretty extern ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf false curried ast;
(* pretty_typ_ast *)
fun pretty_typ_ast {extern_class, extern_type} ctxt _ prtabs trf tokentrf ast =
pretty {extern_class = extern_class, extern_type = extern_type, extern_const = I}
- ctxt (mode_tabs prtabs (print_mode_value ()))
- trf tokentrf true false ast 0;
+ ctxt (mode_tabs prtabs (print_mode_value ())) trf tokentrf true false ast;
end;
--- a/src/Pure/Syntax/syn_ext.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Sun Dec 05 08:34:02 2010 +0100
@@ -10,6 +10,7 @@
val constrainC: string
val typeT: typ
val spropT: typ
+ val default_root: string Config.T
val max_pri: int
val stamp_trfun: stamp -> string * 'a -> string * ('a * stamp)
val mk_trfun: string * 'a -> string * ('a * stamp)
@@ -112,6 +113,9 @@
val any = "any";
val anyT = Type (any, []);
+val default_root =
+ Config.string (Config.declare "Syntax.default_root" (K (Config.String any)));
+
(** datatype xprod **)
--- a/src/Pure/Syntax/syntax.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML Sun Dec 05 08:34:02 2010 +0100
@@ -117,7 +117,7 @@
val standard_parse_term: (term -> string option) ->
(((string * int) * sort) list -> string * int -> Term.sort) ->
(string -> bool * string) -> (string -> string option) -> Proof.context ->
- (string -> bool) -> syntax -> typ -> Symbol_Pos.T list * Position.T -> term
+ syntax -> string -> Symbol_Pos.T list * Position.T -> term
val standard_parse_typ: Proof.context -> syntax ->
((indexname * sort) list -> indexname -> sort) -> Symbol_Pos.T list * Position.T -> typ
val standard_parse_sort: Proof.context -> syntax -> Symbol_Pos.T list * Position.T -> sort
@@ -149,10 +149,8 @@
val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
val update_const_gram: bool -> (string -> bool) ->
mode -> (string * typ * mixfix) list -> syntax -> syntax
- val update_trrules: Proof.context -> (string -> bool) -> syntax ->
- (string * string) trrule list -> syntax -> syntax
- val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
- (string * string) trrule list -> syntax -> syntax
+ val update_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
+ val remove_trrules: Proof.context -> syntax -> (string * string) trrule list -> syntax -> syntax
val update_trrules_i: ast trrule list -> syntax -> syntax
val remove_trrules_i: ast trrule list -> syntax -> syntax
end;
@@ -702,14 +700,13 @@
fun ambiguity_msg pos = "Parse error: ambiguous syntax" ^ Position.str_of pos;
-fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root (syms, pos) =
+fun read_asts ctxt (Syntax (tabs, _)) xids root (syms, pos) =
let
val {lexicon, gram, parse_ast_trtab, ...} = tabs;
val toks = Lexicon.tokenize lexicon xids syms;
val _ = List.app (Lexicon.report_token ctxt) toks;
- val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
- val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
+ val pts = Parser.parse ctxt gram root (filter Lexicon.is_proper toks)
handle ERROR msg =>
error (msg ^
implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
@@ -733,10 +730,10 @@
(* read *)
-fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
+fun read ctxt (syn as Syntax (tabs, _)) root inp =
let
val {parse_ruletab, parse_trtab, ...} = tabs;
- val asts = read_asts ctxt is_logtype syn false (Syn_Ext.typ_to_nonterm ty) inp;
+ val asts = read_asts ctxt syn false root inp;
in
Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
(map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
@@ -778,8 +775,8 @@
map show_term (take limit results)))
end;
-fun standard_parse_term check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
- read ctxt is_logtype syn ty (syms, pos)
+fun standard_parse_term check get_sort map_const map_free ctxt syn root (syms, pos) =
+ read ctxt syn root (syms, pos)
|> map (Type_Ext.decode_term get_sort map_const map_free)
|> disambig ctxt check;
@@ -787,7 +784,7 @@
(* read types *)
fun standard_parse_typ ctxt syn get_sort (syms, pos) =
- (case read ctxt (K false) syn Syn_Ext.typeT (syms, pos) of
+ (case read ctxt syn (Syn_Ext.typ_to_nonterm Syn_Ext.typeT) (syms, pos) of
[t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
| _ => error (ambiguity_msg pos));
@@ -795,7 +792,7 @@
(* read sorts *)
fun standard_parse_sort ctxt syn (syms, pos) =
- (case read ctxt (K false) syn Type_Ext.sortT (syms, pos) of
+ (case read ctxt syn (Syn_Ext.typ_to_nonterm Type_Ext.sortT) (syms, pos) of
[t] => Type_Ext.sort_of_term t
| _ => error (ambiguity_msg pos));
@@ -832,7 +829,7 @@
Ast.str_of_ast lhs ^ " -> " ^ Ast.str_of_ast rhs)
| NONE => rule);
-fun read_pattern ctxt is_logtype syn (root, str) =
+fun read_pattern ctxt syn (root, str) =
let
fun constify (ast as Ast.Constant _) = ast
| constify (ast as Ast.Variable x) =
@@ -842,7 +839,7 @@
val (syms, pos) = read_token str;
in
- (case read_asts ctxt is_logtype syn true root (syms, pos) of
+ (case read_asts ctxt syn true root (syms, pos) of
[ast] => constify ast
| _ => error (ambiguity_msg pos))
end;
@@ -857,8 +854,7 @@
val cert_rules = prep_rules I;
-fun read_rules ctxt is_logtype syn =
- prep_rules (read_pattern ctxt is_logtype syn);
+fun read_rules ctxt syn = prep_rules (read_pattern ctxt syn);
end;
@@ -909,11 +905,11 @@
fun update_const_gram add is_logtype prmode decls =
(if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
-fun update_trrules ctxt is_logtype syn =
- ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
+fun update_trrules ctxt syn =
+ ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt syn;
-fun remove_trrules ctxt is_logtype syn =
- remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
+fun remove_trrules ctxt syn =
+ remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt syn;
val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
--- a/src/Pure/Thy/thy_syntax.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.ML Sun Dec 05 08:34:02 2010 +0100
@@ -60,7 +60,6 @@
| Token.Space => Markup.empty
| Token.Comment => Markup.comment
| Token.InternalValue => Markup.empty
- | Token.Malformed => Markup.malformed
| Token.Error _ => Markup.malformed
| Token.Sync => Markup.control
| Token.EOF => Markup.control;
--- a/src/Pure/sign.ML Sat Dec 04 21:53:00 2010 +0100
+++ b/src/Pure/sign.ML Sun Dec 05 08:34:02 2010 +0100
@@ -499,7 +499,7 @@
fun gen_trrules f args thy = thy |> map_syn (fn syn =>
let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
- in f (ProofContext.init_global thy) (is_logtype thy) syn rules syn end);
+ in f (ProofContext.init_global thy) syn rules syn end);
val add_trrules = gen_trrules Syntax.update_trrules;
val del_trrules = gen_trrules Syntax.remove_trrules;