X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fpxp%2Fpxp%2Fcompatibility%2Fmarkup_document.ml;fp=helm%2FDEVEL%2Fpxp%2Fpxp%2Fcompatibility%2Fmarkup_document.ml;h=bbc4979538f5f63b1990db69a3446140e009a4e1;hb=c03d2c1fdab8d228cb88aaba5ca0f556318bebc5;hp=0000000000000000000000000000000000000000;hpb=758057e85325f94cd88583feb1fdf6b038e35055;p=helm.git

diff --git a/helm/DEVEL/pxp/pxp/compatibility/markup_document.ml b/helm/DEVEL/pxp/pxp/compatibility/markup_document.ml
new file mode 100644
index 000000000..bbc497953
--- /dev/null
+++ b/helm/DEVEL/pxp/pxp/compatibility/markup_document.ml
@@ -0,0 +1,374 @@
+(* $Id$
+ * ----------------------------------------------------------------------
+ *)
+
+type node_type = 
+    T_element of string
+  | T_data
+
+class type [ 'node ] extension = [ 'node ] Pxp_document.extension
+
+class type [ 'ext, 'node ] pxp_extension_type =
+object ('self)
+    method clone : 'self
+    method node : 'self Pxp_document.node
+    method set_node : 'self Pxp_document.node -> unit
+
+    method markup_node : 'node
+    method set_markup_node : 'node -> unit
+
+    method set_index : 'self Pxp_yacc.index -> unit
+    method index : 'self Pxp_yacc.index
+  end
+;;
+
+
+class type [ 'ext ] node = 
+  object ('self)
+    constraint 'ext = 'ext node #extension
+    method pxp_node : (('ext, 'ext node) pxp_extension_type) Pxp_document.node
+
+    method extension : 'ext
+    method delete : unit
+    method parent : 'ext node
+    method root : 'ext node
+    method orphaned_clone : 'ext node
+    method orphaned_flat_clone : 'ext node
+    method add_node : 'ext node -> unit
+    method add_pinstr : Markup_dtd.proc_instruction -> unit
+    method pinstr : string -> Markup_dtd.proc_instruction list
+    method pinstr_names : string list
+    method sub_nodes : 'ext node list
+    method iter_nodes : ('ext node -> unit) -> unit
+    method iter_nodes_sibl :
+      ('ext node option -> 'ext node -> 'ext node option -> unit) -> unit
+    method set_nodes : 'ext node list -> unit
+    method data : string
+    method node_type : node_type
+    method attribute : string -> Markup_types.att_value
+    method attribute_names : string list
+    method attribute_type : string -> Markup_types.att_type
+    method attributes : (string * Markup_types.att_value) list
+    method required_string_attribute : string -> string
+    method required_list_attribute : string -> string list
+    method optional_string_attribute : string -> string option
+    method optional_list_attribute : string -> string list
+    method quick_set_attributes : (string * Markup_types.att_value) list -> unit
+    method find : string -> 'ext node
+    method reset_finder : unit
+    method dtd : Markup_dtd.dtd
+    method create_element :
+      Markup_dtd.dtd -> node_type -> (string * string) list -> 'ext node
+    method create_data : Markup_dtd.dtd -> string -> 'ext node
+    method local_validate : unit
+    method keep_always_whitespace_mode : unit
+    method write_compact_as_latin1 : Markup_types.output_stream -> unit
+    method internal_adopt : 'ext node option -> unit
+    method internal_delete : 'ext node -> unit
+    method internal_init : Markup_dtd.dtd -> string -> (string * string) list -> unit
+  end
+;;
+
+
+class [ 'ext ] pxp_extension init_markup_node =
+  (object (self : 'self)
+    (* constraint 'ext = 'ext node #extension *)
+    val mutable pxp_node = (None : 
+			      'self Pxp_document.node option)
+    (* 'ext pxp_extension Pxp_document.node option *)
+    val mutable markup_node = (init_markup_node : 'ext node)
+
+    val mutable index = (None : 'self Pxp_yacc.index option)
+
+    method clone =
+      {< >}
+
+    method node =
+      match pxp_node with
+          None ->
+            assert false
+        | Some n -> n
+
+    method set_node n =
+      pxp_node <- Some n
+
+    method markup_node = markup_node
+
+    method set_markup_node n = markup_node <- n
+
+    method set_index ix =
+      index <- Some ix
+
+    method index = 
+      match index with
+	  None -> assert false
+	| Some x -> x
+
+   end
+     : ['ext, 'ext node] pxp_extension_type )
+;;
+
+
+class [ 'ext ] emulate_markup_node init_ext init_pxp_node = 
+  object (self)
+    constraint 'ext = 'ext node #extension
+    val mutable pxp_node = (init_pxp_node : 
+			      ('ext, 'ext #node) 
+			      pxp_extension_type Pxp_document.node option)
+    val mutable extension = (init_ext : 'ext)
+
+    method pxp_node =
+      match pxp_node with
+	  None   -> assert false
+	| Some n -> n 
+
+    method extension = extension
+    method delete = self # pxp_node # delete
+    method parent = self # pxp_node # parent # extension # markup_node
+    method root   = self # pxp_node # root # extension # markup_node
+
+    method orphaned_clone =
+      let ext' = extension # clone in
+      let pxp' = self # pxp_node # orphaned_clone in
+      let n = new emulate_markup_node ext' (Some pxp') in
+      ext' # set_node (n : 'ext #node  :> 'ext node);
+      pxp' # extension # set_markup_node n;
+      n
+
+     method orphaned_flat_clone =
+      let ext' = extension # clone in
+      let pxp' = self # pxp_node # orphaned_flat_clone in
+      let n = new emulate_markup_node ext' (Some pxp') in
+      ext' # set_node (n : 'ext #node  :> 'ext node);
+      pxp' # extension # set_markup_node n;
+      n
+
+     method dtd = self # pxp_node # dtd
+
+     method add_node (n : 'ext node) =
+       let n_pxp = n # pxp_node in
+       self # pxp_node # add_node n_pxp
+
+     method add_pinstr pi =
+       self # pxp_node # add_pinstr pi
+
+     method sub_nodes =
+       let l = self # pxp_node # sub_nodes in
+       List.map (fun n_pxp -> n_pxp # extension # markup_node) l
+
+     method pinstr name =
+       self # pxp_node # pinstr name
+
+     method pinstr_names =
+       self # pxp_node # pinstr_names
+
+     method iter_nodes f =
+       self # pxp_node # iter_nodes
+	 (fun n_pxp -> f (n_pxp # extension # markup_node))
+
+     method iter_nodes_sibl f =
+       self # pxp_node # iter_nodes_sibl
+	 (fun left_pxp node_pxp right_pxp ->
+	    let left =
+	      match left_pxp with 
+		  None       -> None
+		| Some n_pxp -> Some (n_pxp # extension # markup_node) in
+	    let right =
+	      match right_pxp with 
+		  None       -> None
+		| Some n_pxp -> Some (n_pxp # extension # markup_node) in
+	    let node =
+	      node_pxp # extension # markup_node in
+	    f left node right
+	 )
+
+     method set_nodes (l : 'ext node list) =
+       let l_pxp = List.map (fun n -> n # pxp_node) l in
+       self # pxp_node # set_nodes l_pxp
+
+     method data = self # pxp_node # data
+
+     method node_type =
+       match self # pxp_node # node_type with
+	   Pxp_document.T_data         -> T_data
+	 | Pxp_document.T_element name -> T_element name
+	 | Pxp_document.T_super_root   -> T_element "-vr"
+	 | Pxp_document.T_pinstr _     -> T_element "-pi"
+	 | _ -> assert false
+
+     method attribute name =
+       self # pxp_node # attribute name
+
+     method attribute_names =
+       self # pxp_node # attribute_names
+
+     method attribute_type name =
+       self # pxp_node # attribute_type name
+
+     method attributes =
+       self # pxp_node # attributes
+
+     method required_string_attribute name =
+       self # pxp_node # required_string_attribute name
+
+     method required_list_attribute name =
+       self # pxp_node # required_list_attribute name
+
+     method optional_string_attribute name =
+       self # pxp_node # optional_string_attribute name
+
+     method optional_list_attribute name =
+       self # pxp_node # optional_list_attribute name
+
+     method quick_set_attributes l =
+       self # pxp_node # quick_set_attributes l
+
+     method find (name : string) =
+       let index = self # root # pxp_node # extension # index in
+       let n = index # find name in (* may raise Not_found *)
+       n # extension # markup_node
+
+     method reset_finder = ()
+
+     method create_element dtd nt atts =
+       let nt_pxp =
+	 match nt with
+	     T_data -> Pxp_document.T_data
+	   | T_element name -> Pxp_document.T_element name in
+       let node_pxp =
+	 self # pxp_node # create_element dtd nt_pxp atts in
+       let ext' = extension # clone in
+       let n = new emulate_markup_node ext' (Some node_pxp) in
+       ext' # set_node (n : 'ext #node  :> 'ext node);
+       node_pxp # extension # set_markup_node n;
+       n
+
+     method create_data dtd s =
+       let node_pxp =
+	 self # pxp_node # create_data dtd s in
+       let ext' = extension # clone in
+       let n = new emulate_markup_node ext' (Some node_pxp) in
+       ext' # set_node (n : 'ext #node  :> 'ext node);
+       node_pxp # extension # set_markup_node n;
+       n
+
+     method keep_always_whitespace_mode =
+       self # pxp_node # keep_always_whitespace_mode
+
+     method write_compact_as_latin1 out =
+       self # pxp_node # write_compact_as_latin1 out
+
+     method local_validate =
+       self # pxp_node # local_validate()
+
+     method internal_adopt (p:'ext node option) =
+       assert false;
+       ()
+
+     method internal_delete (n:'ext node) =
+       assert false;
+       ()
+ 
+     method internal_init (d:Markup_dtd.dtd) (s:string) (atts:(string*string)list) =
+       assert false;
+       ()
+  end
+;;
+
+class [ 'ext ] data_impl ext data =
+  object (self)
+    inherit [ 'ext ] emulate_markup_node ext None
+    constraint 'ext = 'ext node #extension
+    initializer
+      if data <> "" then
+	failwith "Emulation of Markup_document: Cannot instantiate data node with non-empty string";
+      let self' = (self : 'ext #node :> 'ext node ) in
+      pxp_node <- Some (new Pxp_document.data_impl (new pxp_extension self'))
+
+  end
+;;
+
+class [ 'ext ] element_impl ext =
+  object (self)
+    inherit [ 'ext ] emulate_markup_node ext None
+    initializer
+      let self' = (self : 'ext #node :> 'ext node ) in
+      pxp_node <- Some (new Pxp_document.element_impl (new pxp_extension self'))
+  end
+;;
+
+
+class [ 'ext ] document w =
+  object (self)
+    val pxp_doc = new Pxp_document.document 
+		    (w : Markup_types.collect_warnings :> Pxp_types.collect_warnings)
+
+    val mutable standalone_flag = false
+
+    method init_xml_version v =
+      pxp_doc # init_xml_version v
+
+    method xml_version =
+      pxp_doc # xml_version
+
+    method init_xml_standalone b =
+      standalone_flag <- b
+
+    method xml_standalone = standalone_flag
+
+    method init_root (r : 'ext node) =
+      pxp_doc # init_root (r # pxp_node);
+      self # dtd # set_standalone_declaration standalone_flag
+        (* questionable *)
+
+    method root =
+      let pxp_root = pxp_doc # root in
+      pxp_root # extension # markup_node
+
+    method dtd =
+      pxp_doc # dtd
+
+    method add_pinstr pi =
+      pxp_doc # add_pinstr pi
+
+    method pinstr name =
+      pxp_doc # pinstr name
+
+    method pinstr_names =
+      pxp_doc # pinstr_names
+
+    method write_compact_as_latin1 out =
+      pxp_doc # write_compact_as_latin1 out
+
+  end
+;;
+
+(* ======================================================================
+ * History:
+ *
+ * $Log$
+ * Revision 1.1  2000/11/17 09:57:30  lpadovan
+ * Initial revision
+ *
+ * Revision 1.6  2000/08/18 20:19:00  gerd
+ * 	Changed the emulation: there are now wrapper objects for nodes.
+ * This was necessary because node_type changed in PXP such that it became
+ * incompatible with Markup's node_type.
+ *
+ * Revision 1.5  2000/07/14 21:35:35  gerd
+ * 	Updated because of the simplification of Pxp_types.collect_warnings.
+ *
+ * Revision 1.4  2000/07/08 17:40:50  gerd
+ * 	Updated the simulation.
+ *
+ * Revision 1.3  2000/06/14 22:19:27  gerd
+ * 	Update because of additional 'encoding' methods.
+ *
+ * Revision 1.2  2000/05/30 00:08:40  gerd
+ * 	Bugfix.
+ *
+ * Revision 1.1  2000/05/29 23:43:51  gerd
+ * 	Initial compatibility revision.
+ *
+ *)
+