]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/content_pres/cicNotationPres.ml
made "dtd_dir" optional, is needed only by the web server, not by matita
[helm.git] / helm / ocaml / content_pres / cicNotationPres.ml
index cc3a204a4e3874ba3ee55ccb3477932ae66447bc..308f23d22a13ea4826cde1050c8fbdc24a672c04 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
+open Printf
+
 module Ast = CicNotationPt
 module Mpres = Mpresentation
 
@@ -175,31 +179,33 @@ let is_atomic t =
   aux_mpres t
 
 let add_parens child_prec child_assoc child_pos 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
   else if child_prec >= 0
     && (child_prec < curr_prec
       || (child_prec = curr_prec &&
           child_assoc = Gramext.LeftA &&
-          child_pos = `Right)
+          child_pos <> `Left)
       || (child_prec = curr_prec &&
           child_assoc = Gramext.RightA &&
-          child_pos = `Left))
-  then  (* parens should be added *)
-(*     (prerr_endline "adding parens";
-    prerr_endline (Printf.sprintf "child_prec = %d\nchild_assoc = %s\nchild_pos = %s\ncurr_prec= %d"
-      child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos
-      child_pos) curr_prec); *)
+          child_pos <> `Right))
+  then begin (* parens should be added *)
+(*     prerr_endline "adding parens!"; *)
     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])
-  else
+  end else
     t
 
 let render ids_to_uris =
   let module A = Ast in
   let module P = Mpresentation in
-  let use_unicode = true in
+(*   let use_unicode = true in *)
   let lookup_uri id =
     (try
       let uri = Hashtbl.find ids_to_uris id in
@@ -304,7 +310,7 @@ let render ids_to_uris =
     let new_xref = ref [] in
     let new_xmlattrs = ref [] in
     let new_pos = ref pos in
-    let reinit = ref false in
+(*     let reinit = ref false in *)
     let rec aux_attribute =
       function
       | A.AttributedTerm (attr, t) ->
@@ -323,9 +329,9 @@ let render ids_to_uris =
           | None -> aux !new_xmlattrs mathonly new_xref !new_pos prec t
           | Some (child_prec, child_assoc) ->
               let t' = 
-                aux !new_xmlattrs mathonly new_xref !new_pos child_prec t
-              in
-              if !reset then t'
+                aux !new_xmlattrs mathonly new_xref !new_pos child_prec t in
+              if !reset
+              then t'
               else add_parens child_prec child_assoc !new_pos prec t')
     in
     aux_attribute t