diff tools/make_template.ml @ 22:91e247c68ee8

Template generation
author Adam Chlipala <adamc@hcoop.net>
date Fri, 05 Sep 2008 16:46:32 -0400
parents
children c8070689f5ca
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/tools/make_template.ml	Fri Sep 05 16:46:32 2008 -0400
@@ -0,0 +1,41 @@
+let input_line () = 
+  try
+    Some (input_line stdin)
+  with End_of_file -> None
+
+let rec initial last_was_empty =
+  match input_line () with
+  | None -> ()
+  | Some "(* begin thide *)" ->	thide last_was_empty
+  | Some "" ->
+      if not (last_was_empty) then
+	print_newline ();
+      initial true
+  | Some line ->
+      if String.length line >= 2 && line.[0] = '(' && line.[1] = '*' then
+	if line.[String.length line - 2] = '*' && line.[String.length line - 1] = ')' then
+	  initial last_was_empty
+	else
+	  comment last_was_empty
+      else begin
+	print_endline line;
+	initial false
+      end
+
+and comment last_was_empty =
+  match input_line () with
+  | None -> ()
+  | Some line ->
+      if String.length line >= 2 && line.[String.length line - 2] = '*'
+	  && line.[String.length line - 1] = ')' then
+	initial last_was_empty
+      else
+	comment last_was_empty
+
+and thide last_was_empty =
+  match input_line () with
+  | None -> ()
+  | Some "(* end thide *)" -> initial last_was_empty
+  | Some _ -> thide last_was_empty
+
+let () = initial false