X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fpxp%2Fpxp%2Fdoc%2Fmanual%2Fsrc%2Freadme.ent;fp=helm%2FDEVEL%2Fpxp%2Fpxp%2Fdoc%2Fmanual%2Fsrc%2Freadme.ent;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=e9fdfc35a6b507bd603e6cbfeb6e152275af7c8d;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git

diff --git a/helm/DEVEL/pxp/pxp/doc/manual/src/readme.ent b/helm/DEVEL/pxp/pxp/doc/manual/src/readme.ent
deleted file mode 100644
index e9fdfc35a..000000000
--- a/helm/DEVEL/pxp/pxp/doc/manual/src/readme.ent
+++ /dev/null
@@ -1,364 +0,0 @@
-<!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));
-      ]
-    ()
-;;
-'>