snapshot

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 6bc494cdc5801be74a740972c16abf665dd60c9d..681dfd5e50b83b0369445b7e75280ad35620e38f 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -144,7 +144,7 @@ let extract_term_production pattern =
         [NoBinding, symbol "\\ROOT"] @ aux p2 @ [NoBinding, symbol "\\OF"]
         @ aux p1
     | Sqrt p -> [NoBinding, symbol "\\SQRT"] @ aux p
-    | Break -> []
+(*     | Break -> [] *)
     | Box (_, pl) -> List.flatten (List.map aux pl)
   and aux_magic magic =
     match magic with
@@ -323,7 +323,11 @@ EXTEND
           return_term loc (Layout (Box (H, p)))
       | SYMBOL "\\VBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
           return_term loc (Layout (Box (V, p)))
-      | SYMBOL "\\BREAK" -> return_term loc (Layout Break)
+      | SYMBOL "\\HVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box (HV, p)))
+      | SYMBOL "\\HOVBOX"; DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
+          return_term loc (Layout (Box (HOV, p)))
+(*       | SYMBOL "\\BREAK" -> return_term loc (Layout Break) *)
       | DELIM "\\["; p = l1_pattern; DELIM "\\]" ->
           return_term loc (CicNotationUtil.boxify p)
       | p = SELF; SYMBOL "\\AS"; id = IDENT ->