1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
31 | RuleId of CicNotationParser.rule_id
32 | InterpretationId of TermAcicContent.interpretation_id
33 | PrettyPrinterId of TermContentPres.pretty_printer_id
35 let compare_notation_id x y =
37 | RuleId i1, RuleId i2 -> CicNotationParser.compare_rule_id i1 i2
40 | x,y -> Pervasives.compare x y
42 let initial_parser_ref_counter () = RefCounter.create ()
43 let initial_rule_ids_to_items ()= Hashtbl.create 113
45 let parser_ref_counter = ref (initial_parser_ref_counter ());;
46 let rule_ids_to_items = ref (initial_rule_ids_to_items ());;
48 let process_notation st =
50 | Notation (loc, dir, l1, associativity, precedence, l2) ->
52 CicNotationParser.check_l1_pattern
53 l1 (dir = Some `RightToLeft) precedence associativity
55 let item = (l1, precedence, associativity, l2) in
56 let rule_id = ref [] in
58 if dir <> Some `RightToLeft then
59 let create_cb (l1, precedence, associativity, l2) =
61 CicNotationParser.extend l1
63 CicNotationPt.AttributedTerm
64 (`Loc loc,TermContentPres.instantiate_level2 env l2)) in
65 rule_id := [ RuleId id ];
66 Hashtbl.add !rule_ids_to_items id item
68 RefCounter.incr ~create_cb !parser_ref_counter item
71 if dir <> Some `LeftToRight then
73 (TermContentPres.add_pretty_printer
79 | Interpretation (loc, dsc, l2, l3) ->
80 let interp_id = TermAcicContent.add_interpretation dsc l2 l3 in
81 [InterpretationId interp_id]
84 (* CSC: Matita compiled with recent OCaml triggers the assert false in the
85 code below. The exception FOO trick ignores the failure. It seems to
86 work, but it's the classical patch without understanding what the problem
90 let remove_notation = function
91 xxx -> try match xxx with
95 Hashtbl.find !rule_ids_to_items id
96 with Not_found -> raise FOO (*assert false*) in
97 RefCounter.decr ~delete_cb:(fun _ -> CicNotationParser.delete id)
98 !parser_ref_counter item
99 | PrettyPrinterId id -> TermContentPres.remove_pretty_printer id
100 | InterpretationId id -> TermAcicContent.remove_interpretation id
103 let get_all_notations () =
105 (fun (interp_id, dsc) ->
106 InterpretationId interp_id, "interpretation: " ^ dsc)
107 (TermAcicContent.get_all_interpretations ())
109 let get_active_notations () =
110 List.map (fun id -> InterpretationId id)
111 (TermAcicContent.get_active_interpretations ())
113 let set_active_notations ids =
116 (function InterpretationId interp_id -> Some interp_id | _ -> None)
119 TermAcicContent.set_active_interpretations interp_ids
121 let history = ref [];;
124 history := (!parser_ref_counter,!rule_ids_to_items) :: !history;
125 parser_ref_counter := initial_parser_ref_counter ();
126 rule_ids_to_items := initial_rule_ids_to_items ();
127 TermContentPres.push ();
128 TermAcicContent.push ();
129 CicNotationParser.push ()
133 TermContentPres.pop ();
134 TermAcicContent.pop ();
135 CicNotationParser.pop ();
138 | (prc,riti) :: tail ->
139 parser_ref_counter := prc;
140 rule_ids_to_items := riti;