1. bug fixed: Unicode characters that are not mapped to TeX macros used to

   be post-fixed with a blank
2. bug fixed: the textual pretty-printer does not implement the same
   spacing politics of GtkMathView. Since that politics is very very complex
   to implement, I try a different solution: we explicitly insert a space
   where we want one. The widget does not seem to be disturbed by this.
   This way the let ... rec and match ... with constructs are now printed
   correctly and they can be read back.
3. syntax change: applicative patterns no longer require parentheses around
   them

diff --git a/helm/software/components/content_pres/boxPp.ml b/helm/software/components/content_pres/boxPp.ml
index 53149877ea73a1eb71e3c5b2f75ec4f7f78df552..b9bb9fbbd5badc06ef55a36ca418471731559db2 100644 (file)
--- a/helm/software/components/content_pres/boxPp.ml
+++ b/helm/software/components/content_pres/boxPp.ml
@@ -193,13 +193,14 @@ let render_to_strings choose_action size markup =
     | Pres.Mgliph (_, s) -> fixed_rendering s
     | Pres.Mo (_, s) ->
         let s =
-          if String.length s > 1 then
-            (* heuristic to guess which operators need to be expanded in their
-             * TeX like format *)
-            Utf8Macro.tex_of_unicode s ^ " "
-          else s
+         if String.length s = 1 && Char.code s.[0] < 128 then
+          s
+         else
+          match Utf8Macro.tex_of_unicode s with
+             Some s -> s ^ " "
+           | None -> s
         in
-        fixed_rendering s
+         fixed_rendering s
     | Pres.Mspace _ -> fixed_rendering string_space
     | Pres.Mrow (attrs, children) ->
         let children' = List.map aux_mpres children in

diff --git a/helm/software/components/content_pres/cicNotationParser.ml b/helm/software/components/content_pres/cicNotationParser.ml
index 088d1b69d690562e4ce74281f3109cccdee259d0..69ae68aeec37781191993b7e52fd7a447f196803 100644 (file)
--- a/helm/software/components/content_pres/cicNotationParser.ml
+++ b/helm/software/components/content_pres/cicNotationParser.ml
@@ -458,6 +458,7 @@ EXTEND
     [ id = IDENT -> id, None, []
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
         id, None, vars
+    | id = IDENT; vars = LIST1 possibly_typed_name -> id, None, vars
     ]
   ];
   binder: [

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 4198e83b0311b7ed3be2376ff107bed53654b555..673df335f224d4db81427637f1c185bb31e2a9bb 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -357,7 +357,7 @@ let render ids_to_uris ?(prec=(-1)) =
     let attrs = make_href xmlattrs xref in
     (match l with
     | `Symbol s -> Mpres.Mo (attrs, to_unicode s)
-    | `Keyword s -> Mpres.Mo (attrs, to_unicode s)
+    | `Keyword s -> Mpres.Mtext (attrs, to_unicode s)
     | `Number s  -> Mpres.Mn (attrs, to_unicode s))
   and aux_layout mathonly xref pos prec l =
     let attrs = make_xref xref in

diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml
index e925db0aa7085f11e802c23dbbbca2c5bc6d1caa..a8bfe114746f5c9d79968d7c96141de6d8f27646 100644 (file)
--- a/helm/software/components/content_pres/termContentPres.ml
+++ b/helm/software/components/content_pres/termContentPres.ml
@@ -75,6 +75,7 @@ let vbox = box Ast.V
 let hvbox = box Ast.HV
 let hovbox = box Ast.HOV
 let break = Ast.Layout Ast.Break
+let space = Ast.Literal (`Symbol " ")
 let builtin_symbol s = Ast.Literal (`Symbol s)
 let keyword k = add_keyword_attrs (Ast.Literal (`Keyword k))
 
@@ -128,24 +129,26 @@ let pp_ast0 t k =
           match outty_opt with
           | None -> []
           | Some outty ->
-              [ keyword "return"; break; remove_level_info (k outty)]
+              [ space; keyword "return"; space; break; remove_level_info (k outty)]
         in
         let indty_box =
           match indty_opt with
           | None -> []
-          | Some (indty, href) -> [ keyword "in"; break; ident_w_href href indty ]
+          | Some (indty, href) -> [ space; keyword "in"; space; break; ident_w_href href indty ]
         in
         let match_box =
           hvbox false false [
            hvbox false true [
-            hvbox false true [ keyword "match"; break; top_pos (k what) ];
+            hvbox false true [keyword "match"; space; break; top_pos (k what)];
             break;
             hvbox false true indty_box;
             break;
             hvbox false true outty_box
            ];
            break;
-           keyword "with"
+           space;
+           keyword "with";
+           space
          ]
         in
         let mk_case_pattern (head, href, vars) =
@@ -216,7 +219,9 @@ let pp_ast0 t k =
           let (params, name, ty, body) = fst_fun in
           hvbox false true ([
             keyword "let";
+            space;
             keyword rec_op;
+            space;
             name] @
             params @
             (match ty with None -> [] | Some ty -> [builtin_symbol ":"; ty]) @

diff --git a/helm/software/components/grafite_parser/print_grammar.ml b/helm/software/components/grafite_parser/print_grammar.ml
index 6a05865de8f2c9149b6e6a6c6e7ca4b274afd315..f05b77a11b029fa75d60ea5d920793ebca2767fa 100644 (file)
--- a/helm/software/components/grafite_parser/print_grammar.ml
+++ b/helm/software/components/grafite_parser/print_grammar.ml
@@ -28,11 +28,15 @@
 open Gramext 
 
 let tex_of_unicode s =
+(*CSC: ??????? What's the meaning of this function?
   let contractions = ("\\Longrightarrow","=>") :: [] in
   if String.length s <= 1 then s
   else  (* probably an extended unicode symbol *)
     let s = Utf8Macro.tex_of_unicode s in
     try List.assoc s contractions with Not_found -> s
+*) match Utf8Macro.tex_of_unicode s with
+      Some s -> s
+    | None -> s
 
 let needs_brackets t =
   let rec count_brothers = function 

diff --git a/helm/software/components/syntax_extensions/utf8Macro.ml b/helm/software/components/syntax_extensions/utf8Macro.ml
index e5fca10c48cc06e3a428865ea94190758f7cbc3f..36d6b175d713cd213ae540bdb9aa953e8f80efaf 100644 (file)
--- a/helm/software/components/syntax_extensions/utf8Macro.ml
+++ b/helm/software/components/syntax_extensions/utf8Macro.ml
@@ -41,7 +41,10 @@ let unicode_of_tex s =
   with Macro_not_found _ -> s
 
 let tex_of_unicode s =
+ (*WARNING: the space below is a nbsp (0x00A0), not a normal space *)
+ if s = " " then Some ""
+ else
   try
-    "\\" ^ Hashtbl.find Utf8MacroTable.utf82macro s
-  with Not_found -> s
+    Some ("\\" ^ Hashtbl.find Utf8MacroTable.utf82macro s)
+  with Not_found -> None
 

diff --git a/helm/software/components/syntax_extensions/utf8Macro.mli b/helm/software/components/syntax_extensions/utf8Macro.mli
index d92f60b373ac3f8053e7419708a3cb9b53840b52..b21ba504fe125824e8fab675ad2de1de84932a80 100644 (file)
--- a/helm/software/components/syntax_extensions/utf8Macro.mli
+++ b/helm/software/components/syntax_extensions/utf8Macro.mli
@@ -36,5 +36,4 @@ val expand: string -> string
 val unicode_of_tex: string -> string
 
   (** ... the other way round *)
-val tex_of_unicode: string -> string
-
+val tex_of_unicode: string -> string option

diff --git a/helm/software/matita/help/C/sec_terms.xml b/helm/software/matita/help/C/sec_terms.xml
index 65000b9ba8d0859ae25f08d1b04d8febfc12fe04..5f682eb83ccdb6a67ee68199c4565021cd40d412 100644 (file)
--- a/helm/software/matita/help/C/sec_terms.xml
+++ b/helm/software/matita/help/C/sec_terms.xml
@@ -387,6 +387,12 @@
       <entry><emphasis role="bold">(</emphasis>&id; &id; [&id;]…<emphasis role="bold">)</emphasis></entry>
       <entry>n-ary constructor (binds the n arguments)</entry>
      </row>
+     <row>
+      <entry/>
+      <entry>|</entry>
+      <entry>&id; &id; [&id;]…</entry>
+      <entry>n-ary constructor (binds the n arguments)</entry>
+     </row>
     </tbody>
    </tgroup>
   </table>