basic_ag/bagUntrusted.cmi
basic_rg/brg.cmo: common/entity.cmx
basic_rg/brg.cmx: common/entity.cmx
-basic_rg/brgOutput.cmi: lib/log.cmi basic_rg/brg.cmx
+basic_rg/brgOutput.cmi: lib/log.cmi common/library.cmi basic_rg/brg.cmx
basic_rg/brgOutput.cmo: common/output.cmi lib/nUri.cmi lib/log.cmi \
common/library.cmi common/hierarchy.cmi common/entity.cmx lib/cps.cmx \
basic_rg/brg.cmx basic_rg/brgOutput.cmi
TAGS = test test-si test-si-fast hal xml-si-drg xml-si-old
-XMLS = xml/grundlagen/l/not.ld.xml xml/grundlagen/l/et.ld.xml \
- xml/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
- xml/grundlagen/l/e/pairis1.ld.xml
+XMLS = xml/brg/grundlagen/l/not.ld.xml xml/brg/grundlagen/l/et.ld.xml \
+ xml/brg/grundlagen/l/e/st/eq/landau/n/rt/rp/r/c/8283/t234.ld.xml \
+ xml/brg/grundlagen/l/e/pairis1.ld.xml
include Makefile.common
@echo " HELENA -u -x -s 1 $(INPUT)"
$(H)./$(MAIN).opt -u -x -s 1 -S 1 $(INPUT) > etc/log.txt
-
%.ld: BASEURL = --stringparam baseurl $(LDDLURL)
%.ld:
(* term xml printing ********************************************************)
-let rec exp_term c frm = function
+let rec exp_term e t out tab = match t with
| B.Sort (a, l) ->
let a =
let err _ = a in
let f s = Y.Name (s, true) :: a in
H.get_sort err f l
in
- F.fprintf frm "<Sort position=%S%a/>" (string_of_int l) X.old_name a
+ let attrs = [X.position l; X.name a] in
+ X.tag X.sort attrs out tab
| B.LRef (a, i) ->
let a =
let err _ = a in
let f n r = Y.Name (n, r) :: a in
let f _ b = attrs_of_binder (Y.name err f) b in
- B.get err f c i
+ B.get err f e i
in
- F.fprintf frm "<LRef position=%S%a/>" (string_of_int i) X.old_name a
- | B.GRef (a, u) ->
- let a = Y.Name (U.name_of_uri u, true) :: a in
- F.fprintf frm "<GRef uri=%S%a/>" (U.string_of_uri u) X.old_name a
- | B.Cast (a, w, t) ->
- F.fprintf frm "<Cast%a>%a</Cast>@,%a" X.old_name a (exp_boxed c) w (exp_term c) t
+ let attrs = [X.position i; X.name a] in
+ X.tag X.lref attrs out tab
+ | B.GRef (a, n) ->
+ let a = Y.Name (U.name_of_uri n, true) :: a in
+ let attrs = [X.uri n; X.name a] in
+ X.tag X.gref attrs out tab
+ | B.Cast (a, u, t) ->
+ let attrs = [] in
+ X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+ exp_term e t out tab
| B.Appl (a, v, t) ->
- F.fprintf frm "<Appl%a>%a</Appl>@,%a" X.old_name a (exp_boxed c) v (exp_term c) t
- | B.Bind (b, t) ->
- let f b cc = F.fprintf frm "%a@,%a" (exp_bind c) b (exp_term cc) t in
- let f b = B.push (f b) c b in
- rename_bind f c b
+ let attrs = [] in
+ X.tag X.appl attrs ~contents:(exp_term e v) out tab;
+ exp_term e t out tab
+ | B.Bind (b, t) ->
+ let b = rename_bind C.start e b in
+ exp_bind e b out tab;
+ exp_term (B.push C.start e b) t out tab
-and exp_boxed c frm t =
- F.fprintf frm "@,@[<v3> %a@]@," (exp_term c) t
-
-and exp_bind c frm = function
+and exp_bind e b out tab = match b with
| B.Abst (a, w) ->
- F.fprintf frm "<Abst%a>%a</Abst>" X.old_name a (exp_boxed c) w
+ let attrs = [X.name a; X.mark a] in
+ X.tag X.abst attrs ~contents:(exp_term e w) out tab
| B.Abbr (a, v) ->
- F.fprintf frm "<Abbr%a/>%a</Abbr>" X.old_name a (exp_boxed c) v
- | B.Void a ->
- F.fprintf frm "<Void%a/>" X.old_name a
+ let attrs = [X.name a; X.mark a] in
+ X.tag X.abbr attrs ~contents:(exp_term e v) out tab
+ | B.Void a ->
+ let attrs = [X.name a; X.mark a] in
+ X.tag X.void attrs out tab
-let export_term frm t =
- F.fprintf frm "%a" (exp_boxed B.empty_lenv) t
+let export_term = exp_term B.empty_lenv
val specs: (Brg.lenv, Brg.term) Log.specs
+val export_term: Brg.term -> Library.pp
+(*
val export_term: Format.formatter -> Brg.term -> unit
+*)
let path_of_uri uri =
N.concat base (Str.string_after (U.string_of_uri uri) 3)
-let pp_head frm =
- F.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
-
-let pp_doctype frm =
- F.fprintf frm "<!DOCTYPE ENTITY SYSTEM %S>@,@," system
-
-let open_entity si g frm =
- let opts = if si then "si" else "" in
- let f shp =
- F.fprintf frm "<ENTITY hierarchy=%S options=%S>" shp opts
- in
- H.string_of_graph f g
-
-let close_entity frm =
- F.fprintf frm "</ENTITY>"
-
-let name frm a =
- let f s = function
- | true -> F.fprintf frm " name=%S" s
- | false -> F.fprintf frm " name=%S" ("^" ^ s)
- in
- Y.name C.start f a
-
-let pp_entity pp_term frm = function
- | a, u, Y.Abst w ->
- let str = U.string_of_uri u in
- let a = Y.Name (U.name_of_uri u, true) :: a in
- F.fprintf frm "<ABST uri=%S%a>%a</ABST>" str name a pp_term w
- | a, u, Y.Abbr v ->
- let str = U.string_of_uri u in
- let a = Y.Name (U.name_of_uri u, true) :: a in
- F.fprintf frm "<ABBR uri=%S%a>%a</ABBR>" str name a pp_term v
-
-let pp_boxed pp_term frm entity =
- F.fprintf frm "@,@[<v3> %a@]@," (pp_entity pp_term) entity
-
(* interface functions ******************************************************)
-let old_export_entity pp_term si g entity =
- let _, uri, _ = entity in
- let path = path_of_uri uri in
- let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
- let och = open_out (path ^ obj_ext) in
- let frm = F.formatter_of_out_channel och in
- F.pp_set_margin frm max_int;
- F.fprintf frm "@[<v>%t%t%t%a%t@]@."
- pp_head pp_doctype
- (open_entity si g) (pp_boxed pp_term) entity close_entity;
- close_out och
-
-let old_name = name
-
-(****************************************************************************)
-
type och = string -> unit
type attr = string * string
val name: Entity.attrs -> attr
val mark: Entity.attrs -> attr
-
-val old_export_entity:
- (Format.formatter -> 'term -> unit) ->
- bool -> Hierarchy.graph -> 'term Entity.entity -> unit
-
-val old_name: Format.formatter -> Entity.attrs -> unit
(* helpers ******************************************************************)
let mk_uri root s =
- String.concat "/" ["ld:"; "drg"; root; s ^ ".ld"]
+ String.concat "/" ["ld:"; "crg"; root; s ^ ".ld"]
let empty_lenv = ESort
let export_entity si g moch = function
| DrgEntity e -> X.export_entity DO.export_term si g e
- | BrgEntity e -> X.old_export_entity BrgO.export_term si g e
+ | BrgEntity e -> X.export_entity BrgO.export_term si g e
| MetaEntity e ->
begin match moch with
| None -> ()
--- /dev/null
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ -->
+
+<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
+
+<xsl:strip-space elements="ABST ABBR"/>
+
+<xsl:template match="ABST">
+ <h2>
+ <xsl:text>Declaration:</xsl:text>
+ <xsl:call-template name="entity"/>
+ </h2>
+ <div><xsl:apply-templates/></div>
+</xsl:template>
+
+<xsl:template match="ABBR">
+ <h2>
+ <xsl:text>Definition:</xsl:text>
+ <xsl:call-template name="entity"/>
+ </h2>
+ <div><xsl:apply-templates/></div>
+</xsl:template>
+
+</xsl:stylesheet>
+++ /dev/null
-<?xml version="1.0" encoding="UTF-8"?>
-
-<!--
- ||M|| This file is part of HELM, an Hypertextual, Electronic
- ||A|| Library of Mathematics, developed at the Computer Science
- ||T|| Department, University of Bologna, Italy.
- ||I||
- ||T|| HELM is free software; you can redistribute it and/or
- ||A|| modify it under the terms of the GNU General Public License
- \ / version 2 or (at your option) any later version.
- \ / This software is distributed as is, NO WARRANTY.
- V_______________________________________________________________ -->
-
-<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
-
-<xsl:strip-space elements="ABST ABBR VOID"/>
-
-<xsl:template match="ABST">
- <h2>
- <xsl:text>Declaration:</xsl:text>
- <xsl:call-template name="entry"/>
- </h2>
- <div><xsl:apply-templates/></div>
-</xsl:template>
-
-<xsl:template match="ABBR">
- <h2>
- <xsl:text>Definition:</xsl:text>
- <xsl:call-template name="entry"/>
- </h2>
- <div><xsl:apply-templates/></div>
-</xsl:template>
-
-<xsl:template match="VOID">
- <h2>
- <xsl:text>Exclusion:</xsl:text>
- <xsl:call-template name="entry"/>
- </h2>
- <div><xsl:apply-templates/></div>
-</xsl:template>
-
-</xsl:stylesheet>
<xsl:template name="global">
<span style="{$global}">
- <xsl:value-of select="@name"/>
- </span>
+ <a name="" title="{@mark}">
+ <xsl:value-of select="@name"/>
+ </a>
+ </span>
</xsl:template>
<xsl:template name="mk_segment">
</xsl:choose>
</xsl:template>
-<xsl:template name="entry">
+<xsl:template name="entity">
<xsl:call-template name="sp"/>
<xsl:call-template name="global"/>
<xsl:call-template name="sp"/>
<xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform">
-<xsl:strip-space elements="ENTRY"/>
+<xsl:strip-space elements="ENTITY"/>
+
<xsl:template match="/">
<html><head>
<meta content="Ferruccio Guidi" name="author"/>
</body></html>
</xsl:template>
-<xsl:template match="ENTRY">
+<xsl:template match="ENTITY">
<xsl:apply-templates/><h2/>
<div>
Validation parameters:
<xsl:include href="ld-html-library.xsl"/>
<xsl:include href="ld-html-term.xsl"/>
-<xsl:include href="ld-html-entry.xsl"/>
+<xsl:include href="ld-html-entity.xsl"/>
<xsl:include href="ld-html-root.xsl"/>
<xsl:output
<!ATTLIST Sort
position NMTOKEN #REQUIRED
name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!ELEMENT LRef EMPTY>
<!ATTLIST LRef
position NMTOKEN #REQUIRED
name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!ELEMENT GRef EMPTY>
<!ATTLIST GRef
- uri CDATA #REQUIRED
- name CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!ELEMENT Cast %term;>
<!ATTLIST Cast
- name CDATA #IMPLIED
+ name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!ELEMENT Appl %term;>
<!ATTLIST Appl
- name CDATA #IMPLIED
+ name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!ELEMENT Abst %term;>
<!ATTLIST Abst
- name CDATA #IMPLIED
+ name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!ELEMENT Abbr %term;>
<!ATTLIST Abbr
- name CDATA #IMPLIED
+ name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!ELEMENT Void EMPTY>
<!ATTLIST Void
- name CDATA #IMPLIED
+ name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!-- ENVIRONMENT ENTRIES -->
-<!ENTITY % entry '(ABST|ABBR|VOID)'>
+<!ENTITY % entity '(ABST|ABBR)'>
<!ELEMENT ABST %term;>
<!ATTLIST ABST
- uri CDATA #REQUIRED
- name CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!ELEMENT ABBR %term;>
<!ATTLIST ABBR
- uri CDATA #REQUIRED
- name CDATA #IMPLIED
->
-
-<!ELEMENT VOID EMPTY>
-<!ATTLIST VOID
- uri CDATA #REQUIRED
- name CDATA #IMPLIED
+ uri CDATA #REQUIRED
+ name CDATA #IMPLIED
+ mark NMTOKEN #IMPLIED
>
<!-- ROOT -->
-<!ELEMENT ENTRY %entry;>
-<!ATTLIST ENTRY
+<!ELEMENT ENTITY %entity;>
+<!ATTLIST ENTITY
hierarchy NMTOKEN #REQUIRED
options NMTOKENS #IMPLIED
>
projects / helm.git / commitdiff