librarian: retrieval of buildable files speeded up a lot

[helm.git] / helm / software / components / content_pres / cicNotationPres.ml

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 175aae993aca95e502196319f4db119d6388b5cf..8ed430901893a0d2cf8f268b34c6509428e30fbd 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -182,22 +182,23 @@ let is_atomic t =
   aux_mpres t
 
 let add_parens child_prec curr_prec t =
-(*   eprintf
-    ("add_parens: " ^^
-    "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d\n\n%!")
-    child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos)
-    curr_prec; *)
-  if is_atomic t then t
-(* FG: FIXME: should be < but < causes no brackets when \forall .. \to .. associates to the left *)  
-  else if child_prec >= 0 && child_prec <= curr_prec then 
-    begin (* parens should be added *)
-(*      prerr_endline "adding parens!";  *)
+  if is_atomic t then 
+    ((*prerr_endline ("NOT adding parens around ATOMIC: "^
+      BoxPp.render_to_string (function x::_->x|_->assert false)
+        ~map_unicode_to_tex:false 80 t);*)t)
+  else if child_prec >= 0 && child_prec < curr_prec then 
+    begin 
+    (*prerr_endline ("adding parens around: "^
+      BoxPp.render_to_string (function x::_->x|_->assert false)
+        ~map_unicode_to_tex:false 80 t);*)
     match t with
     | Mpresentation.Mobject (_, box) ->
         mpres_of_box (Box.H ([], [ open_box_paren; box; closed_box_paren ]))
     | mpres -> Mpresentation.Mrow ([], [open_paren; t; closed_paren])
   end else
-    t
+    ((*prerr_endline ("NOT adding parens around: "^
+      BoxPp.render_to_string (function x::_->x|_->assert false)
+        ~map_unicode_to_tex:false 80 t);*)t)
 
 let render ids_to_uris ?(prec=(-1)) =
   let module A = Ast in
@@ -322,7 +323,6 @@ let render ids_to_uris ?(prec=(-1)) =
     let expected_level = ref None in
     let new_xref = ref [] in
     let new_xmlattrs = ref [] in
-(*     let reinit = ref false in *)
     let rec aux_attribute =
       function
       | A.AttributedTerm (attr, t) ->
@@ -346,12 +346,17 @@ let render ids_to_uris ?(prec=(-1)) =
           (match !inferred_level with
           | None -> aux !new_xmlattrs mathonly new_xref prec t 
           | Some child_prec ->
-              let t' = 
-                aux !new_xmlattrs mathonly new_xref child_prec t in
+              let t' = aux !new_xmlattrs mathonly new_xref child_prec t in
+              (*prerr_endline 
+                ("inferred: "^string_of_int child_prec^ 
+                 " exp: "^string_of_int prec ^ 
+                 " term: "^BoxPp.render_to_string ~map_unicode_to_tex:false
+                    (function x::_->x|_->assert false) 80 t');*)
               if !reset
-              then t'
+              then ((*prerr_endline "reset";*)t')
               else add_parens child_prec prec t')
     in
+(*     prerr_endline (CicNotationPp.pp_term t); *)
     aux_attribute t
   and aux_literal xmlattrs xref prec l =
     let attrs = make_href xmlattrs xref in
@@ -375,6 +380,12 @@ let render ids_to_uris ?(prec=(-1)) =
     | A.Atop (t1, t2) ->
         Mpres.Mfrac (atop_attributes @ attrs, invoke_reinit t1,
           invoke_reinit t2)
+    | A.InfRule (t1, t2, t3) ->
+       Mpres.Mrow (attrs,
+        [Mpres.Mfrac ([],
+           Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t1),
+           Mpres.Mstyle ([None,"scriptlevel","0"],invoke_reinit t2));
+         Mpres.Mstyle ([None,"scriptlevel","2"],invoke_reinit t3)])
     | A.Sqrt t -> Mpres.Msqrt (attrs, invoke_reinit t)
     | A.Root (t1, t2) ->
         Mpres.Mroot (attrs, invoke_reinit t1, invoke_reinit t2)