]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/pxp/pxp/doc/manual/src/readme.ent
Initial revision
[helm.git] / helm / DEVEL / pxp / pxp / doc / manual / src / readme.ent
diff --git a/helm/DEVEL/pxp/pxp/doc/manual/src/readme.ent b/helm/DEVEL/pxp/pxp/doc/manual/src/readme.ent
new file mode 100644 (file)
index 0000000..e9fdfc3
--- /dev/null
@@ -0,0 +1,364 @@
+<!ENTITY readme.code.header '
+open Pxp_types
+open Pxp_document
+'>
+<!ENTITY readme.code.footnote-printer '
+class type footnote_printer =
+  object
+    method footnote_to_html : store_type -&gt; out_channel -&gt; unit
+  end
+
+and store_type =
+  object
+    method alloc_footnote : footnote_printer -&gt; int
+    method print_footnotes : out_channel -&gt; unit
+  end
+;;
+'>
+<!ENTITY readme.code.store '
+class store =
+  object (self)
+
+    val mutable footnotes = ( [] : (int * footnote_printer) list )
+    val mutable next_footnote_number = 1
+
+    method alloc_footnote n =
+      let number = next_footnote_number in
+      next_footnote_number &lt;- number+1;
+      footnotes &lt;- footnotes @ [ number, n ];
+      number
+
+    method print_footnotes ch =
+      if footnotes &lt;&gt; [] then begin
+       output_string ch "&lt;hr align=left noshade=noshade width=\"30&percent;\"&gt;\n";
+       output_string ch "&lt;dl&gt;\n";
+       List.iter
+         (fun (_,n) -&gt; 
+            n # footnote_to_html (self : #store_type :&gt; store_type) ch)
+         footnotes;
+       output_string ch "&lt;/dl&gt;\n";
+      end
+
+  end
+;;
+'>
+<!ENTITY readme.code.escape-html '
+let escape_html s =
+  Str.global_substitute
+    (Str.regexp "&lt;\\|&gt;\\|&amp;\\|\"")
+    (fun s -&gt;
+      match Str.matched_string s with
+        "&lt;" -&gt; "&amp;lt;"
+      | "&gt;" -&gt; "&amp;gt;"
+      | "&amp;" -&gt; "&amp;amp;"
+      | "\"" -&gt; "&amp;quot;"
+      | _ -&gt; assert false)
+    s
+;;
+'>
+<!ENTITY readme.code.shared '
+class virtual shared =
+  object (self)
+
+    (* --- default_ext --- *)
+
+    val mutable node = (None : shared node option)
+
+    method clone = {&lt; &gt;} 
+    method node =
+      match node with
+          None -&gt;
+            assert false
+        | Some n -&gt; n
+    method set_node n =
+      node &lt;- Some n
+
+    (* --- virtual --- *)
+
+    method virtual to_html : store -&gt; out_channel -&gt; unit
+
+  end
+;;
+'>
+<!ENTITY readme.code.only-data '
+class only_data =
+  object (self)
+    inherit shared
+
+    method to_html store ch =
+      output_string ch (escape_html (self # node # data))
+  end
+;;
+'>
+<!ENTITY readme.code.no-markup '
+class no_markup =
+  object (self)
+    inherit shared
+
+    method to_html store ch =
+      List.iter
+       (fun n -&gt; n # extension # to_html store ch)
+       (self # node # sub_nodes)
+  end
+;;
+'>
+<!ENTITY readme.code.readme '
+class readme =
+  object (self)
+    inherit shared
+
+    method to_html store ch =
+      (* output header *)
+      output_string 
+       ch "&lt;!DOCTYPE HTML PUBLIC \"-//W3C//DTD HTML 3.2 Final//EN\"&gt;";
+      output_string
+       ch "&lt;!-- WARNING! This is a generated file, do not edit! --&gt;\n";
+      let title = 
+       match self # node # attribute "title" with
+           Value s -&gt; s
+         | _ -&gt; assert false
+      in
+      let html_header, _ =
+       try (self # node # dtd # par_entity "readme:html:header") 
+            # replacement_text
+       with WF_error _ -&gt; "", false in
+      let html_trailer, _ =
+       try (self # node # dtd # par_entity "readme:html:trailer")
+            # replacement_text
+       with WF_error _ -&gt; "", false in
+      let html_bgcolor, _ =
+       try (self # node # dtd # par_entity "readme:html:bgcolor")
+            # replacement_text
+       with WF_error _ -&gt; "white", false in
+      let html_textcolor, _ =
+       try (self # node # dtd # par_entity "readme:html:textcolor")
+            # replacement_text
+       with WF_error _ -&gt; "", false in
+      let html_alinkcolor, _ =
+       try (self # node # dtd # par_entity "readme:html:alinkcolor")
+            # replacement_text
+       with WF_error _ -&gt; "", false in
+      let html_vlinkcolor, _ =
+       try (self # node # dtd # par_entity "readme:html:vlinkcolor")
+            # replacement_text
+       with WF_error _ -&gt; "", false in
+      let html_linkcolor, _ =
+       try (self # node # dtd # par_entity "readme:html:linkcolor")
+            # replacement_text
+       with WF_error _ -&gt; "", false in
+      let html_background, _ =
+       try (self # node # dtd # par_entity "readme:html:background")
+            # replacement_text
+       with WF_error _ -&gt; "", false in
+
+      output_string ch "&lt;html&gt;&lt;header&gt;&lt;title&gt;\n";
+      output_string ch (escape_html title);
+      output_string ch "&lt;/title&gt;&lt;/header&gt;\n";
+      output_string ch "&lt;body ";
+      List.iter
+       (fun (name,value) -&gt;
+          if value &lt;&gt; "" then 
+            output_string ch (name ^ "=\"" ^ escape_html value ^ "\" "))
+       [ "bgcolor",    html_bgcolor;
+         "text",       html_textcolor;
+         "link",       html_linkcolor;
+         "alink",      html_alinkcolor;
+         "vlink",      html_vlinkcolor;
+       ];
+      output_string ch "&gt;\n";
+      output_string ch html_header;
+      output_string ch "&lt;h1&gt;";
+      output_string ch (escape_html title);
+      output_string ch "&lt;/h1&gt;\n";
+      (* process main content: *)
+      List.iter
+       (fun n -&gt; n # extension # to_html store ch)
+       (self # node # sub_nodes);
+      (* now process footnotes *)
+      store # print_footnotes ch;
+      (* trailer *)
+      output_string ch html_trailer;
+      output_string ch "&lt;/html&gt;\n";
+
+  end
+;;
+'>
+<!ENTITY readme.code.section '
+class section the_tag =
+  object (self)
+    inherit shared
+
+    val tag = the_tag
+
+    method to_html store ch =
+      let sub_nodes = self # node # sub_nodes in
+      match sub_nodes with
+         title_node :: rest -&gt;
+           output_string ch ("&lt;" ^ tag ^ "&gt;\n");
+           title_node # extension # to_html store ch;
+           output_string ch ("\n&lt;/" ^ tag ^ "&gt;");
+           List.iter
+             (fun n -&gt; n # extension # to_html store ch)
+             rest
+       | _ -&gt;
+           assert false
+  end
+;;
+
+class sect1 = section "h1";;
+class sect2 = section "h3";;
+class sect3 = section "h4";;
+'>
+<!ENTITY readme.code.map-tag '
+class map_tag the_target_tag =
+  object (self)
+    inherit shared
+
+    val target_tag = the_target_tag
+
+    method to_html store ch =
+      output_string ch ("&lt;" ^ target_tag ^ "&gt;\n");
+      List.iter
+       (fun n -&gt; n # extension # to_html store ch)
+       (self # node # sub_nodes);
+      output_string ch ("\n&lt;/" ^ target_tag ^ "&gt;");
+  end
+;;
+
+class p = map_tag "p";;
+class em = map_tag "b";;
+class ul = map_tag "ul";;
+class li = map_tag "li";;
+'>
+<!ENTITY readme.code.br '
+class br =
+  object (self)
+    inherit shared
+
+    method to_html store ch =
+      output_string ch "&lt;br&gt;\n";
+      List.iter
+       (fun n -&gt; n # extension # to_html store ch)
+       (self # node # sub_nodes);
+  end
+;;
+'>
+<!ENTITY readme.code.code '
+class code =
+  object (self)
+    inherit shared
+
+    method to_html store ch =
+      let data = self # node # data in
+      (* convert tabs *)
+      let l = String.length data in
+      let rec preprocess i column =
+       (* this is very ineffective but comprehensive: *)
+       if i &lt; l then
+         match data.[i] with
+             &apos;\t&apos; -&gt;
+               let n = 8 - (column mod 8) in
+               String.make n &apos; &apos; ^ preprocess (i+1) (column + n)
+           | &apos;\n&apos; -&gt;
+               "\n" ^ preprocess (i+1) 0
+           | c -&gt;
+               String.make 1 c ^ preprocess (i+1) (column + 1)
+       else
+         ""
+      in
+      output_string ch "&lt;p&gt;&lt;pre&gt;";
+      output_string ch (escape_html (preprocess 0 0));
+      output_string ch "&lt;/pre&gt;&lt;/p&gt;";
+
+  end
+;;
+'>
+<!ENTITY readme.code.a '
+class a =
+  object (self)
+    inherit shared
+
+    method to_html store ch =
+      output_string ch "&lt;a ";
+      let href =
+       match self # node # attribute "href" with
+           Value v -&gt; escape_html v
+         | Valuelist _ -&gt; assert false
+         | Implied_value -&gt;
+             begin match self # node # attribute "readmeref" with
+                 Value v -&gt; escape_html v ^ ".html"
+               | Valuelist _ -&gt; assert false
+               | Implied_value -&gt;
+                   ""
+             end
+      in
+      if href &lt;&gt; "" then
+       output_string ch ("href=\""  ^ href ^ "\"");
+      output_string ch "&gt;";
+      output_string ch (escape_html (self # node # data));
+      output_string ch "&lt;/a&gt;";
+       
+  end
+;;
+'>
+<!ENTITY readme.code.footnote '
+class footnote =
+  object (self)
+    inherit shared
+
+    val mutable footnote_number = 0
+
+    method to_html store ch =
+      let number = 
+       store # alloc_footnote (self : #shared :&gt; footnote_printer) in
+      let foot_anchor = 
+       "footnote" ^ string_of_int number in
+      let text_anchor =
+       "textnote" ^ string_of_int number in
+      footnote_number &lt;- number;
+      output_string ch ( "&lt;a name=\"" ^ text_anchor ^ "\" href=\"#" ^ 
+                        foot_anchor ^ "\"&gt;[" ^ string_of_int number ^ 
+                        "]&lt;/a&gt;" )
+
+    method footnote_to_html store ch =
+      (* prerequisite: we are in a definition list &lt;dl&gt;...&lt;/dl&gt; *)
+      let foot_anchor = 
+       "footnote" ^ string_of_int footnote_number in
+      let text_anchor =
+       "textnote" ^ string_of_int footnote_number in
+      output_string ch ("&lt;dt&gt;&lt;a name=\"" ^ foot_anchor ^ "\" href=\"#" ^ 
+                       text_anchor ^ "\"&gt;[" ^ string_of_int footnote_number ^ 
+                       "]&lt;/a&gt;&lt;/dt&gt;\n&lt;dd&gt;");
+      List.iter
+       (fun n -&gt; n # extension # to_html store ch)
+       (self # node # sub_nodes);
+      output_string ch ("\n&lt;/dd&gt;")
+  end
+;;
+'>
+<!ENTITY readme.code.tag-map '
+open Pxp_yacc
+
+let tag_map =
+  make_spec_from_alist
+    ~data_exemplar:(new data_impl (new only_data))
+    ~default_element_exemplar:(new element_impl (new no_markup))
+    ~element_alist:
+      [ "readme", (new element_impl (new readme));
+       "sect1",  (new element_impl (new sect1));
+       "sect2",  (new element_impl (new sect2));
+       "sect3",  (new element_impl (new sect3));
+       "title",  (new element_impl (new no_markup));
+       "p",      (new element_impl (new p));
+       "br",     (new element_impl (new br));
+       "code",   (new element_impl (new code));
+       "em",     (new element_impl (new em));
+       "ul",     (new element_impl (new ul));
+       "li",     (new element_impl (new li));
+       "footnote", (new element_impl (new footnote : #shared :&gt; shared));
+       "a",      (new element_impl (new a));
+      ]
+    ()
+;;
+'>