[Hol-checkins] CVS: hol98/tools/holdoc holdoc-guide.txt,1.27,1.28 holdoc_init.ml,1.16,1.17 holdoc_init.mli,1.12,1.13 holdoc_munge.ml,1.61,1.62

[Keith W. <kw...@us...>]

Update of /cvsroot/hol/hol98/tools/holdoc
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv6510

Modified Files:
	holdoc-guide.txt holdoc_init.ml holdoc_init.mli 
	holdoc_munge.ml 
Log Message:
Netsem internal:

New directive [NO]COMMENTS which allows non-TeX comments (i.e.,
comments of the form (* .. *), as opposed to (*: .. :*) ) to be turned
off in LTS rules.  Special magic to make sure that if a line now
contains nothing but whitespace, it is removed.



Index: holdoc-guide.txt
===================================================================
RCS file: /cvsroot/hol/hol98/tools/holdoc/holdoc-guide.txt,v
retrieving revision 1.27
retrieving revision 1.28
diff -b -C2 -d -r1.27 -r1.28
*** holdoc-guide.txt	26 Jun 2003 16:55:53 -0000	1.27
--- holdoc-guide.txt	26 Mar 2004 11:52:37 -0000	1.28
***************
*** 231,234 ****
--- 231,241 ----
  
  
+ (*[ COMMENTS ]*) turns on comments mode (this is on by default).  This
+ means that, within an lts_to_latex rule, non-TeX comments (* foo *)
+ will be displayed.  (TeX comments (*: foo :*) are unaffected).
+ 
+ (*[ NOCOMMENTS ]*) turns off comments mode.
+ 
+ 
  HOLDoc supports "modes".  All the various lists defined above, and
  also [NO]INDENT, [NO_]SMART_PREFIX, and [NO]RULES are not global; they

Index: holdoc_init.ml
===================================================================
RCS file: /cvsroot/hol/hol98/tools/holdoc/holdoc_init.ml,v
retrieving revision 1.16
retrieving revision 1.17
diff -b -C2 -d -r1.16 -r1.17
*** holdoc_init.ml	26 Jun 2003 16:55:53 -0000	1.16
--- holdoc_init.ml	26 Mar 2004 11:52:37 -0000	1.17
***************
*** 22,25 ****
--- 22,26 ----
    iNDENT : bool ref;
    rULES : bool ref;
+   cOMMENTS : bool ref;
  }
  
***************
*** 41,44 ****
--- 42,46 ----
    iNDENT = ref true;
    rULES = ref false;
+   cOMMENTS = ref true;
  }
  
***************
*** 69,72 ****
--- 71,75 ----
                                         iNDENT = ref !(!curmodals.iNDENT);
                                         rULES = ref !(!curmodals.rULES);
+                                        cOMMENTS = ref !(!curmodals.cOMMENTS);
                                       };
                         modes := (name,!curmodals)::!modes)
***************
*** 183,186 ****
--- 186,191 ----
    | "RULES"           -> !curmodals.rULES := true
    | "NORULES"         -> !curmodals.rULES := false
+   | "COMMENTS"        -> !curmodals.cOMMENTS := true
+   | "NOCOMMENTS"      -> !curmodals.cOMMENTS := false
    (* other *)
    | "ECHO"            -> eCHO := true

Index: holdoc_init.mli
===================================================================
RCS file: /cvsroot/hol/hol98/tools/holdoc/holdoc_init.mli,v
retrieving revision 1.12
retrieving revision 1.13
diff -b -C2 -d -r1.12 -r1.13
*** holdoc_init.mli	26 Jun 2003 16:55:53 -0000	1.12
--- holdoc_init.mli	26 Mar 2004 11:52:37 -0000	1.13
***************
*** 18,21 ****
--- 18,22 ----
    iNDENT : bool ref;
    rULES : bool ref;
+   cOMMENTS : bool ref;
  }
  

Index: holdoc_munge.ml
===================================================================
RCS file: /cvsroot/hol/hol98/tools/holdoc/holdoc_munge.ml,v
retrieving revision 1.61
retrieving revision 1.62
diff -b -C2 -d -r1.61 -r1.62
*** holdoc_munge.ml	24 Mar 2004 14:26:26 -0000	1.61
--- holdoc_munge.ml	26 Mar 2004 11:52:37 -0000	1.62
***************
*** 31,34 ****
--- 31,40 ----
    | _            -> false
  
+ let isComment t =
+   match t with
+     Comment(_) -> true
+   | _          -> false
+ 
+ 
  let gensymcnt = ref 0
  
***************
*** 813,816 ****
--- 819,837 ----
    | []     -> None
  
+ (* possibly strip non-TeX comments from a block *)
+ 
+ let strip xss =
+   if !(!curmodals.cOMMENTS) then
+     xss
+   else
+     let interesting = function
+         Indent(_) -> false
+       | White(_)  -> false
+       | _         -> true
+     in
+     let ($) f g x = f (g x)
+     in
+     List.filter (List.exists interesting) (List.map (List.filter (not $ isComment)) xss)
+ 
  (* output (munge) a whole rule *)
  
***************
*** 831,838 ****
        print_string ("{"^texify n^"}{"^texifys " " rp^": "^texifys " " cat^"}");
        print_string ("{"^(match desc with Some d -> munge pvs d [] | None -> "")^"}\n");
!       print_string ("{"^munges pvs lhs^"}\n");
        print_string ("{"^mungelab pvs lab^"}\n");
!       print_string ("{"^munges pvs rhs^"}\n");
!       print_string ("{"^munges pvs side^"}\n");
        print_string "{";
        (match comm with
--- 852,859 ----
        print_string ("{"^texify n^"}{"^texifys " " rp^": "^texifys " " cat^"}");
        print_string ("{"^(match desc with Some d -> munge pvs d [] | None -> "")^"}\n");
!       print_string ("{"^munges pvs (strip lhs)^"}\n");
        print_string ("{"^mungelab pvs lab^"}\n");
!       print_string ("{"^munges pvs (strip rhs)^"}\n");
!       print_string ("{"^munges pvs (strip side)^"}\n");
        print_string "{";
        (match comm with
***************
*** 853,857 ****
        let texname = gendefname()
        in
!       print_string ("\\newcommand{\\"^texname^"}{\\ddefn{"^namepart^"}{"^munges pvs e^"}\n}\n\n");
        [texname]
  
--- 874,878 ----
        let texname = gendefname()
        in
!       print_string ("\\newcommand{\\"^texname^"}{\\ddefn{"^namepart^"}{"^munges pvs (strip e)^"}\n}\n\n");
        [texname]