raise (HExtlib.Localized
(floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
-type parsable = Grammar.parsable
+type parsable = Grammar.parsable * Ulexing.lexbuf
let parsable_statement status buf =
let grammar = CicNotationParser.level2_ast_grammar status in
- Grammar.parsable grammar (Obj.magic buf)
+ Grammar.parsable grammar (Obj.magic buf), buf
let parse_statement grafite_parser parsable =
exc_located_wrapper
- (fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) parsable))
+ (fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) (fst parsable)))
+
+let strm_of_parsable (_,buf) = buf
let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
]];
grafite_ncommand: [ [
- IDENT "qed" -> G.NQed loc
+ IDENT "qed" ; b = OPT SYMBOL "-" ->
+ let b = match b with None -> true | Some _ -> false in
+ G.NQed (loc,b)
| nflavour = ntheorem_flavour; name = IDENT; SYMBOL ":"; typ = term;
body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
G.NObj (loc, N.Theorem (nflavour, name, typ, body,`Regular))
G.NUnivConstraint (loc,u1,u2)
| IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
G.UnificationHint (loc, t, n)
- | IDENT "coercion"; name = IDENT; SYMBOL ":"; ty = term;
+ | IDENT "coercion"; name = IDENT;
+ compose = OPT [ IDENT "nocomposites" -> () ];
+ SYMBOL ":"; ty = term;
SYMBOL <:unicode<def>>; t = term; "on";
id = [ IDENT | PIDENT ]; SYMBOL ":"; source = term;
"to"; target = term ->
- G.NCoercion(loc,name,t,ty,(id,source),target)
+ let compose = compose = None in
+ G.NCoercion(loc,name,compose,t,ty,(id,source),target)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
G.NObj (loc, N.Record (params,name,ty,fields))
| IDENT "copy" ; s = IDENT; IDENT "from"; u = URI; "with";