From: Ferruccio Guidi Date: Sun, 13 Jul 2014 21:35:30 +0000 (+0000) Subject: - xhtbl : support for named anchors (id's) and other improvements X-Git-Tag: make_still_working~874 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3167db4903eea2eddc60a91cfd922be3672ce077;p=helm.git - xhtbl : support for named anchors (id's) and other improvements - ld_web: additions for the "documentation" page --- diff --git a/helm/www/lambdadelta/BTM.html b/helm/www/lambdadelta/BTM.html index d21660ea7..338b38399 100644 --- a/helm/www/lambdadelta/BTM.html +++ b/helm/www/lambdadelta/BTM.html @@ -223,6 +223,6 @@

-
Last update: Sun, 13 Jul 2014 15:47:14 +0200
+
Last update: Sun, 13 Jul 2014 23:25:31 +0200
diff --git a/helm/www/lambdadelta/apps_2.html b/helm/www/lambdadelta/apps_2.html index 40e52f117..eb58a004c 100644 --- a/helm/www/lambdadelta/apps_2.html +++ b/helm/www/lambdadelta/apps_2.html @@ -191,6 +191,6 @@

-
Last update: Sun, 13 Jul 2014 15:47:14 +0200
+
Last update: Sun, 13 Jul 2014 23:25:31 +0200
diff --git a/helm/www/lambdadelta/basic_2.html b/helm/www/lambdadelta/basic_2.html index b858c6cc3..d3356642f 100644 --- a/helm/www/lambdadelta/basic_2.html +++ b/helm/www/lambdadelta/basic_2.html @@ -1300,6 +1300,6 @@

-
Last update: Sun, 13 Jul 2014 15:47:14 +0200
+
Last update: Sun, 13 Jul 2014 23:25:31 +0200
diff --git a/helm/www/lambdadelta/bin/xhtbl/matrix.ml b/helm/www/lambdadelta/bin/xhtbl/matrix.ml index 62f6b194e..1c65c5004 100644 --- a/helm/www/lambdadelta/bin/xhtbl/matrix.ml +++ b/helm/www/lambdadelta/bin/xhtbl/matrix.ml @@ -7,7 +7,8 @@ type cell = { ck: T.text list; (* contents *) cc: T.css; (* css classes *) cu: T.uri; (* uri *) - cx: T.ext; (* extension *) + cx: T.ext; (* extension *) + cn: T.anchor; (* named anchor *) cb: T.border; (* border *) } @@ -17,8 +18,10 @@ type matrix = { m: cell array array; (* matrix *) } +let strand a b = if a = "" then b else a + let empty = { - ck = []; cc = []; cu = ""; cx = ""; cb = T.border false; + ck = []; cc = []; cu = ""; cx = ""; cn = ""; cb = T.border false; } let make ts = { @@ -29,11 +32,12 @@ let make ts = { let set_key m y x kl = m.m.(y).(x) <- {m.m.(y).(x) with ck = kl} -let set_attrs m y x c u e = +let set_attrs m y x c u e n = m.m.(y).(x) <- {m.m.(y).(x) with cc = c @ m.m.(y).(x).cc; cu = u ^ m.m.(y).(x).cu; cx = m.m.(y).(x).cx ^ e; + cn = strand m.m.(y).(x).cn n; } let set_west m y x b = diff --git a/helm/www/lambdadelta/bin/xhtbl/pass2.ml b/helm/www/lambdadelta/bin/xhtbl/pass2.ml index 2e003ccb3..549d7654e 100644 --- a/helm/www/lambdadelta/bin/xhtbl/pass2.ml +++ b/helm/www/lambdadelta/bin/xhtbl/pass2.ml @@ -54,7 +54,7 @@ let set_attrs st t = let rec aux y x = if y >= t.T.ts.T.rf then () else if x >= t.T.ts.T.cf then aux (succ y) 0 else begin - M.set_attrs st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc t.T.tu t.T.tx; + M.set_attrs st.tm (t.T.ts.T.y + y) (t.T.ts.T.x + x) t.T.tc t.T.tu t.T.tx t.T.tn; aux y (succ x) end in diff --git a/helm/www/lambdadelta/bin/xhtbl/pass3.ml b/helm/www/lambdadelta/bin/xhtbl/pass3.ml index 337437709..d2455a30a 100644 --- a/helm/www/lambdadelta/bin/xhtbl/pass3.ml +++ b/helm/www/lambdadelta/bin/xhtbl/pass3.ml @@ -22,6 +22,7 @@ let process_cell st y x c = (A.get_attr L.concat [] st.c y x) (A.get_attr (S.concat "") "" st.u y x) (A.get_attr (S.concat "") "" st.x y x) + "" let process_row st y row = V.iteri (process_cell st y) row diff --git a/helm/www/lambdadelta/bin/xhtbl/table.ml b/helm/www/lambdadelta/bin/xhtbl/table.ml index fe15c94db..d3ee13bfa 100644 --- a/helm/www/lambdadelta/bin/xhtbl/table.ml +++ b/helm/www/lambdadelta/bin/xhtbl/table.ml @@ -4,6 +4,8 @@ type uri = string type ext = string +type anchor = string + type absolute = bool type size = { @@ -30,6 +32,7 @@ type key = Text of text list | Glue of int option type table = { + tn: anchor; (* named anchor *) mutable tc: css; (* css classes *) mutable tu: uri; (* uri *) mutable tx: ext; (* uri extension *) @@ -54,14 +57,14 @@ let border b = { n = b; s = b; e = b; w = b; } -let mk_key k tc tu tx = { +let mk_key k tc tu tx tn = { ts = no_size; tb = border false; te = Key k; - tc = tc; tu = tu; tx = tx; + tc = tc; tu = tu; tx = tx; tn = tn; ti = id (); } -let mk_line b tl tc tu tx = { +let mk_line b tl tc tu tx tn = { ts = no_size; tb = border b; te = Line (b, tl); - tc = tc; tu = tu; tx = tx; + tc = tc; tu = tu; tx = tx; tn = tn; ti = id (); } diff --git a/helm/www/lambdadelta/bin/xhtbl/textParser.mly b/helm/www/lambdadelta/bin/xhtbl/textParser.mly index 587395988..9072c2b23 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textParser.mly +++ b/helm/www/lambdadelta/bin/xhtbl/textParser.mly @@ -72,9 +72,9 @@ ext: ; table: - | css uri ext key { T.mk_key $4 $1 $2 $3 } - | css uri ext OC tables CC { T.mk_line false $5 $1 $2 $3 } - | css uri ext OB tables CB { T.mk_line true $5 $1 $2 $3 } + | css uri ext name key { T.mk_key $5 $1 $2 $3 $4 } + | css uri ext OC tables CC { T.mk_line false $5 $1 $2 $3 "" } + | css uri ext OB tables CB { T.mk_line true $5 $1 $2 $3 "" } ; tables: diff --git a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml index 339a9aeec..cf7724cdd 100644 --- a/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/textUnparser.ml @@ -44,6 +44,10 @@ let css tc = let uri tu tx = P.sprintf "@\"%s\" \"%s\"" tu tx +let name tn = + P.sprintf "$\"%s\"" tn + + let text = function | T.Plain s -> P.sprintf "\"%s\"" s | T.Link (true, uri, s) -> P.sprintf "@(\"%s\" \"%s\")" uri s @@ -62,8 +66,8 @@ let entry = function let open_table st t = let str = - P.sprintf "%s[{#%u: %s; %s; %s; %s}\n" - (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc) (uri t.T.tu t.T.tx) + P.sprintf "%s[{#%u: %s; %s; %s; %s; %s}\n" + (indent st) t.T.ti (size t.T.ts) (border t.T.tb) (css t.T.tc) (uri t.T.tu t.T.tx) (name t.T.tn) in st.out str; add st diff --git a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml index e46682c3f..0ff801e93 100644 --- a/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml +++ b/helm/www/lambdadelta/bin/xhtbl/xmlUnparser.ml @@ -14,6 +14,13 @@ let myself = F.basename (Sys.argv.(0)) let msg = P.sprintf "This file was generated by %s, do not edit" myself +let compose uri ext = + try + let i = S.index uri '#' in + let uri, fragment = S.sub uri 0 i, S.sub uri i (S.length uri - i) in + uri ^ ext ^ fragment + with Not_found -> uri ^ ext + let border cell = let str = S.make 4 'n' in if cell.M.cb.T.n then str.[0] <- 's'; @@ -26,9 +33,12 @@ let text baseuri ext = function | T.Plain s -> s | T.Link (true, uri, s) -> P.sprintf "%s" uri s | T.Link (false, uri, s) -> - let uri = !O.baseuri ^ baseuri ^ uri ^ ext in + let uri = !O.baseuri ^ baseuri ^ compose uri ext in P.sprintf "%s" uri s +let name cell = + if cell.M.cn = "" then "" else P.sprintf " id=\"%s\"" cell.M.cn + let key cell = if cell.M.ck = [] then "
" else S.concat "" (L.map (text cell.M.cu cell.M.cx) cell.M.ck) @@ -36,8 +46,8 @@ let ind i = S.make (2 * i) ' ' let out_cell och cell = let cc = border cell in - P.fprintf och "%s%s\n" - (ind (i+4)) (S.concat " " cc) (key cell) + P.fprintf och "%s%s\n" + (ind (i+4)) (S.concat " " cc) (name cell) (key cell) let out_row och row = P.fprintf och "%s\n" (ind (i+3)); diff --git a/helm/www/lambdadelta/css/ld_web.css b/helm/www/lambdadelta/css/ld_web.css index 5897aedc6..7ee236c53 100644 --- a/helm/www/lambdadelta/css/ld_web.css +++ b/helm/www/lambdadelta/css/ld_web.css @@ -85,6 +85,20 @@ img.w3c { height: 32px; /* this should be 31px */ } +/* alignment ****************************************************************/ + +td.top { + vertical-align: top; +} + +td.middle { + vertical-align: middle; +} + +td.bottom { + vertical-align: bottom; +} + /* background colors ********************************************************/ .gray { diff --git a/helm/www/lambdadelta/ground_2.html b/helm/www/lambdadelta/ground_2.html index 684c81c6c..680b83770 100644 --- a/helm/www/lambdadelta/ground_2.html +++ b/helm/www/lambdadelta/ground_2.html @@ -234,6 +234,6 @@

-
Last update: Sun, 13 Jul 2014 15:47:14 +0200
+
Last update: Sun, 13 Jul 2014 23:25:31 +0200
diff --git a/helm/www/lambdadelta/index.html b/helm/www/lambdadelta/index.html index 2520a4102..808aff0c9 100644 --- a/helm/www/lambdadelta/index.html +++ b/helm/www/lambdadelta/index.html @@ -202,6 +202,6 @@

-
Last update: Sun, 13 Jul 2014 16:13:35 +0200
+
Last update: Sun, 13 Jul 2014 23:25:31 +0200
diff --git a/helm/www/lambdadelta/news.html b/helm/www/lambdadelta/news.html index 8391452ae..8c30c357e 100644 --- a/helm/www/lambdadelta/news.html +++ b/helm/www/lambdadelta/news.html @@ -302,6 +302,6 @@

-
Last update: Sun, 13 Jul 2014 15:59:00 +0200
+
Last update: Sun, 13 Jul 2014 23:25:31 +0200
diff --git a/helm/www/lambdadelta/version_1.html b/helm/www/lambdadelta/version_1.html index b76aab942..a96ad7126 100644 --- a/helm/www/lambdadelta/version_1.html +++ b/helm/www/lambdadelta/version_1.html @@ -186,6 +186,6 @@

-
Last update: Sun, 13 Jul 2014 15:47:14 +0200
+
Last update: Sun, 13 Jul 2014 23:25:31 +0200
diff --git a/helm/www/lambdadelta/version_2.html b/helm/www/lambdadelta/version_2.html index 8c71c51d8..0435540bf 100644 --- a/helm/www/lambdadelta/version_2.html +++ b/helm/www/lambdadelta/version_2.html @@ -151,6 +151,6 @@

-
Last update: Sun, 13 Jul 2014 15:59:00 +0200
+
Last update: Sun, 13 Jul 2014 23:25:31 +0200
diff --git a/helm/www/lambdadelta/xslt/ld_web_root.xsl b/helm/www/lambdadelta/xslt/ld_web_root.xsl index 43e612301..2eef8f149 100644 --- a/helm/www/lambdadelta/xslt/ld_web_root.xsl +++ b/helm/www/lambdadelta/xslt/ld_web_root.xsl @@ -118,6 +118,15 @@ + + [basic lambdadelta] + + +