in
let match_box =
hvbox false false [
- hvbox false true [
+ hvbox false false [
hvbox false true [keyword "match"; space; break; top_pos (k what)];
break;
hvbox false true indty_box;
keyword "let"; space;
hvbox false true [
aux_var var; space;
- builtin_symbol "\\def"; break; top_pos (k s) ];
- break; space; keyword "in"; space ];
+ builtin_symbol "\\def"; break; top_pos (k s); space; keyword "in"; space ];
+ ];
break;
k t ])
| Ast.LetRec (rec_kind, funs, where) ->
type db = {
level1_patterns21: NotationPt.term IntMap.t;
- compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t option;
+ compiled21: ((NotationPt.term -> (NotationEnv.t * NotationPt.term list * int) option)) Lazy.t;
pattern21_matrix: (NotationPt.term * pattern_id) list;
counter: pattern_id
}
let initial_db = {
level1_patterns21 = IntMap.empty;
- compiled21 = None;
+ compiled21 = lazy (Content2presMatcher.Matcher21.compiler []);
pattern21_matrix = [];
counter = ~-1
}
end
let get_compiled21 status =
- match status#content_pres_db.compiled21 with
- | None -> assert false
- | Some f -> Lazy.force f
+ Lazy.force status#content_pres_db.compiled21
let set_compiled21 status f =
status#set_content_pres_db
- { status#content_pres_db with compiled21 = Some f }
+ { status#content_pres_db with compiled21 = f }
let add_idrefs =
List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))