Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Roqc/ide/rocqide/protocol/   (Beweissystem des Inria Version 9.1.0©)  Datei vom 15.8.2025 mit Größe 3 kB image not shown  

Quelle  xml_printer.ml   Sprache: SML

 
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Xml_datatype

type xml = Xml_datatype.xml

type target = TChannel of out_channel | TBuffer of Buffer.t

type t = target

let make x = x

let buffer_pcdata tmp text =
  let puts = Buffer.add_string tmp in
  let putc = Buffer.add_char tmp in
  let l = String.length text in
  for p = 0 to l-1 do
    match text.[p] with
      | ' ' -> puts " ";
      | '>' -> puts ">"
      | '<' -> puts "<"
      | '&' ->
        if p < l - 1 && text.[p + 1] = '#' then
          putc '&'
        else
          puts "&"
      | '\'' -> puts "'"
      | '"' -> puts """
      | c -> putc c
  done

let buffer_attr tmp (n,v) =
  let puts = Buffer.add_string tmp in
  let putc = Buffer.add_char tmp in
  putc ' ';
  puts n;
  puts "=\"";
  let l = String.length v in
  for p = 0 to l - 1 do
    match v.[p] with
      | '\\' -> puts "\\\\"
      | '"' -> puts "\\\""
      | '<' -> puts "<"
      | '&' -> puts "&"
      | c -> putc c
  done;
  putc '"'

let to_buffer tmp x =
  let pcdata = ref false in
  let puts = Buffer.add_string tmp in
  let putc = Buffer.add_char tmp in
  let rec loop = function
    | Element (tag,alist,[]) ->
      putc '<';
      puts tag;
      List.iter (buffer_attr tmp) alist;
      puts "/>";
      pcdata := false;
    | Element (tag,alist,l) ->
      putc '<';
      puts tag;
      List.iter (buffer_attr tmp) alist;
      putc '>';
      pcdata := false;
      List.iter loop l;
      puts ";
      puts tag;
      putc '>';
      pcdata := false;
    | PCData text ->
      if !pcdata then putc ' ';
      buffer_pcdata tmp text;
      pcdata := true;
  in
  loop x

let pcdata_to_string s =
  let b = Buffer.create 13 in
  buffer_pcdata b s;
  Buffer.contents b

let to_string x =
  let b = Buffer.create 200 in
  to_buffer b x;
  Buffer.contents b

let to_string_fmt x =
  let tmp = Buffer.create 200 in
  let puts = Buffer.add_string tmp in
  let putc = Buffer.add_char tmp in
  let rec loop ?(newl=false) tab = function
    | Element (tag, alist, []) ->
      puts tab;
      putc '<';
      puts tag;
      List.iter (buffer_attr tmp) alist;
      puts "/>";
      if newl then putc '\n';
    | Element (tag, alist, [PCData text]) ->
      puts tab;
      putc '<';
      puts tag;
      List.iter (buffer_attr tmp) alist;
      puts ">";
      buffer_pcdata tmp text;
      puts ";
      puts tag;
      putc '>';
      if newl then putc '\n';
    | Element (tag, alist, l) ->
      puts tab;
      putc '<';
      puts tag;
      List.iter (buffer_attr tmp) alist;
      puts ">\n";
      List.iter (loop ~newl:true (tab^" ")) l;
      puts tab;
      puts ";
      puts tag;
      putc '>';
      if newl then putc '\n';
    | PCData text ->
      buffer_pcdata tmp text;
      if newl then putc '\n';
  in
  loop "" x;
  Buffer.contents tmp

let print t xml =
  let tmp, flush = match t with
    | TChannel oc ->
      let b = Buffer.create 200 in
      b, (fun () -> Buffer.output_buffer oc b; flush oc)
    | TBuffer b ->
      b, (fun () -> ())
  in
  to_buffer tmp xml;
  flush ()

Messung V0.5
C=91 H=99 G=94

¤ Dauer der Verarbeitung: 0.3 Sekunden  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.