X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2FrecommOutput.ml;h=e93935e4aae510784a54a4c3082490b333bbd15b;hb=caf822cbe34e204e6d1b72e272373b561c1a565a;hp=e0f3f1d70397327d87a3dd60e1181a238e44cdb7;hpb=4d232392091ee233afc26ecf3120dd5f5c6a33c8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
index e0f3f1d70..e93935e4a 100644
--- a/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
+++ b/matita/matita/contribs/lambdadelta/bin/recomm/recommOutput.ml
@@ -1,3 +1,4 @@
+module EL = RecommLib
 module ET = RecommTypes
 
 let width = ref 78
@@ -13,8 +14,8 @@ let string_length_utf8 s =
   in
   l - aux 0 0
 
-let complete s =
-  let l = !width - string_length_utf8 s - 6 in
+let complete s n =
+  let l = !width - string_length_utf8 s - 5 - n in
   if l < 0 then begin
     Printf.eprintf "overfull: %S\n" s;
     ""
@@ -23,21 +24,24 @@ let complete s =
   end
 
 let out_src och = function
-  | ET.Line s             ->
+  | ET.Line s                ->
     Printf.fprintf och "%s" s
-  | ET.Text s             ->
+  | ET.Text s                ->
     Printf.fprintf och "%s" s
-  | ET.Mark s             ->
+  | ET.Mark s                ->
     Printf.fprintf och "(* *%s*)" s
-  | ET.Key (s1, s2)       ->
-    Printf.fprintf och "(* %s%s*)" s1 s2
-  | ET.Title ss           ->
+  | ET.Key (s1, s2)          ->
+    let s3 =
+      if s1 = "NOTE" then complete (s1^s2) 0 else ""
+    in
+    Printf.fprintf och "(* %s%s%s*)" s1 s2 s3
+  | ET.Title ss              ->
     let s = String.concat " " ss in
-    Printf.fprintf och "(* %s %s*)" s (complete s)
-  | ET.Slice ss           ->
+    Printf.fprintf och "(* %s %s*)" s (complete s 1)
+  | ET.Slice ss              ->
     let s = String.capitalize_ascii (String.concat " " ss) in
-    Printf.fprintf och "(* %s %s*)" s (complete s)
-  | ET.Other (s1, s2, s3) ->
+    Printf.fprintf och "(* %s %s*)" s (complete s 1)
+  | ET.Other (_, s1, s2, s3) ->
     Printf.fprintf och "%s%s%s" s1 s2 s3
 
 let write_srcs file srcs =
@@ -52,3 +56,41 @@ let write_srcs file srcs =
   let och = open_out target in
   List.iter (out_src och) srcs;
   close_out och
+
+let write_subst och n s =
+  Printf.fprintf och "%s %s\n" s n
+
+let rec write_fst och = function
+  | []                                                    -> ()
+  | ET.Other (2, _, s, _) :: ET.Line _ :: ET.Text t :: tl ->
+    write_snd och tl s (EL.split_on_char ' ' t)
+  | ET.Other (2, _, s, _) :: tl                           ->
+    Printf.eprintf "skipping fst: %S\n" s;
+    write_fst och tl
+  | _ :: tl                                  -> write_fst och tl
+
+and write_snd och tl s = function
+  | "axiom" :: n :: _
+  | "definition" :: n :: _
+  | "corec" :: "definition" :: n :: _
+  | "rec" :: "definition" :: n :: _
+  | "fact" :: n :: _
+  | "corec" :: "fact" :: n :: _
+  | "lemma" :: n :: _
+  | "corec" :: "lemma" :: n :: _
+  | "theorem" :: n :: _
+  | "corec" :: "theorem" :: n :: _
+  | "inductive" :: n :: _
+  | "coinductive" :: n :: _
+  | "|" :: n :: _                     ->
+    let ss = EL.split_on_char ' ' s in
+    List.iter (write_subst och n) (List.tl ss);
+    write_fst och tl
+  | t :: _       ->
+    Printf.eprintf "skipping snd: %S %S\n" s t;
+    write_fst och tl
+  | []             ->
+    Printf.eprintf "skipping snd: %S\n" s;
+    write_fst och tl
+
+let write_substs = write_fst