X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2FtxtCrg.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Ftext%2FtxtCrg.ml;h=ce3853fcb479f6317a8cfc25beb4362f7ddc4ce6;hb=fa5cd121c672589afc0ac8ddd5d184897a38c7c6;hp=980b74a08302db7565957933d512ab65c0664666;hpb=5280ec9794de75e63ffc01bddf1756ebcca02be0;p=helm.git

diff --git a/helm/software/lambda-delta/src/text/txtCrg.ml b/helm/software/lambda-delta/src/text/txtCrg.ml
index 980b74a08..ce3853fcb 100644
--- a/helm/software/lambda-delta/src/text/txtCrg.ml
+++ b/helm/software/lambda-delta/src/text/txtCrg.ml
@@ -105,24 +105,24 @@ let xlate_term f st lenv t =
    TT.contract (xlate_term f st lenv) t
 
 let mk_contents n tt = function
-   | T.Decl -> [], E.Abst (n, tt)
-   | T.Ax   -> [], E.Abst (n, tt)
-   | T.Cong -> [], E.Abst (n, tt)   
-   | T.Def  -> [], E.Abbr tt
-   | T.Th   -> [], E.Abbr tt
+   | T.Decl -> []                    , E.Abst (n, tt)
+   | T.Ax   -> [E.InProp]            , E.Abst (n, tt)
+   | T.Cong -> [E.InProp; E.Progress], E.Abst (n, tt)   
+   | T.Def  -> []                    , E.Abbr tt
+   | T.Th   -> [E.InProp]            , E.Abbr tt
 
 let xlate_entity err f gen st = function
-   | T.Require _                  ->
+   | T.Require _                           ->
       err st
-   | T.Section (Some name)        ->
+   | T.Section (Some name)                 ->
       err {st with path = name :: st.path}
-   | T.Section None               ->
+   | T.Section None                        ->
       begin match st.path with
 	 | _ :: ptl -> 
 	    err {st with path = ptl}
          | _        -> assert false
       end
-   | T.Sorts sorts                ->
+   | T.Sorts sorts                         ->
       let map st (xix, s) =
          let ix = match xix with 
 	    | None    -> st.sort
@@ -131,20 +131,23 @@ let xlate_entity err f gen st = function
          {st with sort = H.set_sorts ix [s]}
       in
       err (List.fold_left map st sorts)
-   | T.Graph id                      ->
+   | T.Graph id                            ->
       assert (H.set_graph id); err st
-   | T.Entity (kind, n, id, meta, t) ->
+   | T.Entity (main, kind, n, id, info, t) ->
       let uri = uri_of_id st id st.path in
       Hashtbl.add henv id uri;
       let tt = xlate_term C.start st D.empty_lenv t in
 (*
       print_newline (); CrgOutput.pp_term print_string tt;
 *)
-      let a, b = mk_contents n tt kind in 
-      let a = if meta <> "" then E.Meta meta :: a else a in
+      let a = [] in
+      let ms, b = mk_contents n tt kind in 
+      let ms = if main then E.Main :: ms else ms in 
+      let a = if ms <> [] then E.Meta ms :: a else a in
+      let a = if info <> ("", "") then E.Info info :: a else a in
       let entity = E.Mark st.line :: a, uri, b in
       f {st with line = succ st.line} entity
-   | T.Generate _                   ->
+   | T.Generate _                          ->
       err st
 
 (* Interface functions ******************************************************)