common/output.cmx: common/options.cmx lib/log.cmx common/output.cmi
common/entity.cmo: common/options.cmx lib/nUri.cmi automath/aut.cmx
common/entity.cmx: common/options.cmx lib/nUri.cmx automath/aut.cmx
+common/marks.cmo: common/entity.cmx
+common/marks.cmx: common/entity.cmx
+common/alpha.cmi: common/entity.cmx
+common/alpha.cmo: common/entity.cmx common/alpha.cmi
+common/alpha.cmx: common/entity.cmx common/alpha.cmi
common/library.cmi: common/entity.cmx
common/library.cmo: lib/nUri.cmi common/hierarchy.cmi common/entity.cmx \
lib/cps.cmx common/library.cmi
basic_rg/brgEnvironment.cmx basic_rg/brg.cmx basic_rg/brgUntrusted.cmi
complete_rg/crg.cmo: common/entity.cmx
complete_rg/crg.cmx: common/entity.cmx
-complete_rg/crgOutput.cmi: common/library.cmi complete_rg/crg.cmx
-complete_rg/crgOutput.cmo: lib/nUri.cmi common/library.cmi \
- common/hierarchy.cmi common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
+complete_rg/crgOutput.cmi: complete_rg/crg.cmx
+complete_rg/crgOutput.cmo: lib/nUri.cmi common/hierarchy.cmi \
+ common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
complete_rg/crgOutput.cmi
-complete_rg/crgOutput.cmx: lib/nUri.cmx common/library.cmx \
- common/hierarchy.cmx common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
+complete_rg/crgOutput.cmx: lib/nUri.cmx common/hierarchy.cmx \
+ common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
complete_rg/crgOutput.cmi
+complete_rg/crgXml.cmi: common/library.cmi complete_rg/crg.cmx
+complete_rg/crgXml.cmo: lib/nUri.cmi common/library.cmi common/hierarchy.cmi \
+ common/entity.cmx complete_rg/crg.cmx lib/cps.cmx common/alpha.cmi \
+ complete_rg/crgXml.cmi
+complete_rg/crgXml.cmx: lib/nUri.cmx common/library.cmx common/hierarchy.cmx \
+ common/entity.cmx complete_rg/crg.cmx lib/cps.cmx common/alpha.cmx \
+ complete_rg/crgXml.cmi
complete_rg/crgTxt.cmi: text/txt.cmx complete_rg/crg.cmx
complete_rg/crgTxt.cmo: text/txtTxt.cmi text/txt.cmx common/options.cmx \
lib/nUri.cmi common/hierarchy.cmi common/entity.cmx complete_rg/crg.cmx \
complete_rg/crgAut.cmx: common/options.cmx lib/nUri.cmx common/entity.cmx \
complete_rg/crg.cmx lib/cps.cmx automath/aut.cmx complete_rg/crgAut.cmi
complete_rg/crgBrg.cmi: complete_rg/crg.cmx basic_rg/brg.cmx
-complete_rg/crgBrg.cmo: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
- basic_rg/brg.cmx complete_rg/crgBrg.cmi
-complete_rg/crgBrg.cmx: common/entity.cmx complete_rg/crg.cmx lib/cps.cmx \
- basic_rg/brg.cmx complete_rg/crgBrg.cmi
+complete_rg/crgBrg.cmo: common/marks.cmx common/entity.cmx \
+ complete_rg/crg.cmx lib/cps.cmx basic_rg/brg.cmx complete_rg/crgBrg.cmi
+complete_rg/crgBrg.cmx: common/marks.cmx common/entity.cmx \
+ complete_rg/crg.cmx lib/cps.cmx basic_rg/brg.cmx complete_rg/crgBrg.cmi
toplevel/meta.cmo: common/entity.cmx
toplevel/meta.cmx: common/entity.cmx
toplevel/metaOutput.cmi: toplevel/meta.cmx
toplevel/metaOutput.cmi toplevel/metaLibrary.cmi toplevel/metaBrg.cmi \
toplevel/metaBag.cmi toplevel/metaAut.cmi toplevel/meta.cmx lib/log.cmi \
common/library.cmi common/hierarchy.cmi common/entity.cmx \
- complete_rg/crgTxt.cmi complete_rg/crgOutput.cmi complete_rg/crgBrg.cmi \
+ complete_rg/crgXml.cmi complete_rg/crgTxt.cmi complete_rg/crgBrg.cmi \
complete_rg/crgAut.cmi complete_rg/crg.cmx lib/cps.cmx \
basic_rg/brgUntrusted.cmi basic_rg/brgReduction.cmi \
basic_rg/brgOutput.cmi basic_rg/brg.cmx basic_ag/bagUntrusted.cmi \
toplevel/metaOutput.cmx toplevel/metaLibrary.cmx toplevel/metaBrg.cmx \
toplevel/metaBag.cmx toplevel/metaAut.cmx toplevel/meta.cmx lib/log.cmx \
common/library.cmx common/hierarchy.cmx common/entity.cmx \
- complete_rg/crgTxt.cmx complete_rg/crgOutput.cmx complete_rg/crgBrg.cmx \
+ complete_rg/crgXml.cmx complete_rg/crgTxt.cmx complete_rg/crgBrg.cmx \
complete_rg/crgAut.cmx complete_rg/crg.cmx lib/cps.cmx \
basic_rg/brgUntrusted.cmx basic_rg/brgReduction.cmx \
basic_rg/brgOutput.cmx basic_rg/brg.cmx basic_ag/bagUntrusted.cmx \
-options hierarchy output entity library
+options hierarchy output entity marks alpha library
--- /dev/null
+(*
+ ||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_______________________________________________________________ *)
+
+module Y = Entity
+
+(* internal functions *******************************************************)
+
+let rec rename ns n =
+ let token, mode = n in
+ let n = token ^ "_", mode in
+ if List.mem n ns then rename ns n else n
+
+let alpha_name acc attr =
+ let ns, a = acc in
+ match attr with
+ | Y.Name n ->
+ if List.mem n ns then
+ let n = rename ns n in
+ n :: ns, Y.Name n :: a
+ else
+ n :: ns, attr :: a
+ | _ -> assert false
+
+(* interface functions ******************************************************)
+
+let alpha ns a =
+ let f a names =
+ let _, names = List.fold_left alpha_name (ns, []) (List.rev names) in
+ List.rev_append a names
+ in
+ Y.get_names f a
--- /dev/null
+(*
+ ||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_______________________________________________________________ *)
+
+val alpha: Entity.names -> Entity.attrs -> Entity.attrs
type uri = NUri.uri
type id = Aut.id
+type name = id * bool (* token, real? *)
-type attr = Name of id * bool (* name, real? *)
+type names = name list
+
+type attr = Name of name (* name *)
| Apix of int (* additional position index *)
| Mark of int (* node marker *)
| Meta of string (* metaliguistic annotation *)
| _ :: tl -> priv err f tl
| [] -> err ()
+let rec meta err f = function
+ | Meta s :: _ -> f s
+ | _ :: tl -> meta err f tl
+ | [] -> err ()
+
let resolve err f name a =
let rec aux i = function
| Name (n, true) :: _ when n = name -> f i
in
aux 0 a
+let rec rev_append_names ns = function
+ | [] -> ns
+ | Name n :: tl -> rev_append_names (n :: ns) tl
+ | _ :: tl -> rev_append_names ns tl
+
let xlate f xlate_term = function
| a, uri, Abst t ->
let f t = f (a, uri, Abst t) in xlate_term f t
let refresh_status st = {st with
si = !O.si; expand = !O.expand
}
+
let f i = "mark", string_of_int i in
Y.mark err f a
+(* TODO: the string s must be quoted *)
+let meta a =
+ let err () = "meta", "" in
+ let f s = "meta", s in
+ Y.meta err f a
+
let export_entity pp_term si xdir (a, u, b) =
let path = path_of_uri xdir u in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
let out = output_string och in
xml out "1.0" "UTF-8"; doctype out root system;
let a = Y.Name (U.name_of_uri u, true) :: a in
- let attrs = [uri u; name a; mark a] in
+ let attrs = [uri u; name a; mark a; meta a] in
let contents = match b with
| Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
| Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
val name: Entity.attrs -> attr
val mark: Entity.attrs -> attr
+
+val meta: Entity.attrs -> attr
--- /dev/null
+(*
+ ||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_______________________________________________________________ *)
+
+module Y = Entity
+
+(* interface functions ******************************************************)
+
+let new_location =
+ let location = ref 0 in
+ fun () -> incr location; !location
+
+let new_mark () =
+ Y.Mark (new_location ())
-crg crgOutput crgTxt crgAut crgBrg
+crg crgOutput crgXml crgTxt crgAut crgBrg
(* kernel version: complete, relative, global *)
(* note : fragment of complete lambda-delta serving as abstract layer *)
-type uri = Entity.uri
-type id = Entity.id
-type attrs = Entity.attrs
+module Y = Entity
+
+type uri = Y.uri
+type id = Y.id
+type attrs = Y.attrs
type bind = Abst of term list (* domains *)
| Abbr of term list (* bodies *)
| EProj of lenv * attrs * lenv (* environment, attrs, closure *)
| EBind of lenv * attrs * bind (* environment, attrs, binder *)
-type entity = term Entity.entity
+type entity = term Y.entity
(* helpers ******************************************************************)
| EBind (tl, a, _) ->
let err kk = aux f (succ i) (k + kk) tl in
let f j = f i j (k + j) in
- Entity.resolve err f id a
+ Y.resolve err f id a
| EProj _ -> assert false (* TODO *)
in
aux f 0 0 lenv
| ESort -> err i
| EBind (_, a, _) when i = 0 ->
let err () = err i in
- Entity.get_name err f j a
+ Y.get_name err f j a
| EBind (tl, _, _) ->
get_name err f (pred i) j tl
| EProj (tl, _, e) ->
let rec aux f i k = function
| ESort -> err i
| EBind (_, a, _) when i = 0 ->
- if Entity.count_names a > j then f (k + j) else err i
+ if Y.count_names a > j then f (k + j) else err i
| EBind (tl, a, _) ->
- aux f (pred i) (k + Entity.count_names a) tl
+ aux f (pred i) (k + Y.count_names a) tl
| EProj _ -> assert false (* TODO *)
in
aux f i 0 lenv
+
+let rec names_of_lenv ns = function
+ | ESort -> ns
+ | EBind (tl, a, _) -> names_of_lenv (Y.rev_append_names ns a) tl
+ | EProj (tl, _, e) -> names_of_lenv (names_of_lenv ns e) tl
module C = Cps
module Y = Entity
+module M = Marks
module D = Crg
module B = Brg
+(* internal functions: crg to brg term **************************************)
+
let rec lenv_fold_left map1 map2 x = function
| D.ESort -> x
| D.EBind (tl, a, b) -> lenv_fold_left map1 map2 (map1 x a b) tl
match b with
| D.Abst ws ->
let map x n w =
- let f ww = B.Bind (n :: a, B.Abst ww, x) in xlate_term f w
+ let f ww = B.Bind (n :: M.new_mark () :: a, B.Abst ww, x) in
+ xlate_term f w
in
List.fold_left2 map x ns ws
| D.Abbr vs ->
let map x n v =
- let f vv = B.Bind (n :: a, B.Abbr vv, x) in xlate_term f v
+ let f vv = B.Bind (n :: a, B.Abbr vv, x) in
+ xlate_term f v
in
List.fold_left2 map x ns vs
| D.Void _ ->
and xlate_proj x _ e =
lenv_fold_left xlate_bind xlate_proj x e
+(* internal functions: brg to crg term **************************************)
+
+let rec xlate_bk_term f = function
+ | B.Sort (a, l) -> f (D.TSort (a, l))
+ | B.GRef (a, n) -> f (D.TGRef (a, n))
+ | B.LRef (a, i) -> f (D.TLRef (a, i, 0))
+ | B.Cast (a, u, t) ->
+ let f uu tt = f (D.TCast (a, uu, tt)) in
+ let f uu = xlate_bk_term (f uu) t in
+ xlate_bk_term f u
+ | B.Appl (a, u, t) ->
+ let f uu tt = f (D.TAppl (a, [uu], tt)) in
+ let f uu = xlate_bk_term (f uu) t in
+ xlate_bk_term f u
+ | B.Bind (a, b, t) ->
+ let f bb tt = f (D.TBind (a, bb, tt)) in
+ let f bb = xlate_bk_term (f bb) t in
+ xlate_bk_bind f b
+
+and xlate_bk_bind f = function
+ | B.Abst t ->
+ let f tt = f (D.Abst [tt]) in
+ xlate_bk_term f t
+ | B.Abbr t ->
+ let f tt = f (D.Abbr [tt]) in
+ xlate_bk_term f t
+ | B.Void -> f (D.Void 1)
+
+(* interface functions ******************************************************)
+
let brg_of_crg f t =
f (xlate_term C.start t)
+
+let crg_of_brg = xlate_bk_term
V_______________________________________________________________ *)
val brg_of_crg: (Brg.term -> 'a) -> Crg.term -> 'a
+
+val crg_of_brg: (Crg.term -> 'a) -> Brg.term -> 'a
module C = Cps
module H = Hierarchy
module Y = Entity
-module X = Library
module D = Crg
(****************************************************************************)
| D.EBind (x, a, y) -> pp_lenv out x; pp_attrs out a; pp_bind out y
(****************************************************************************)
-
-let rec list_iter map l out tab = match l with
- | [] -> ()
- | hd :: tl -> map hd out tab; list_iter map tl out tab
-
-let list_rev_iter map e ns l out tab =
- let rec aux err f e = function
- | [], [] -> f e
- | n :: ns, hd :: tl ->
- let f e =
-(*
- pp_lenv print_string e; print_string " |- ";
- pp_term print_string hd; print_newline ();
-*)
- map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
- in
- aux err f e (ns, tl)
- | _ -> err ()
- in
- ignore (aux C.err C.start e (ns, l))
-
-let lenv_iter map1 map2 l out tab =
- let rec aux f = function
- | D.ESort -> f ()
- | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
- | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
- in
- aux C.start l
-
-let rec exp_term e t out tab = match t with
- | D.TSort (a, l) ->
- let a =
- let err _ = a in
- let f s = Y.Name (s, true) :: a in
- H.string_of_sort err f l
- in
- let attrs = [X.position l; X.name a] in
- X.tag X.sort attrs out tab
- | D.TLRef (a, i, j) ->
- let a =
- let err _ = a in
- let f n r = Y.Name (n, r) :: a in
- D.get_name err f i j e
- in
- let attrs = [X.position i; X.offset j; X.name a] in
- X.tag X.lref attrs out tab
- | D.TGRef (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
- | D.TCast (a, u, t) ->
- let attrs = [] in
- X.tag X.cast attrs ~contents:(exp_term e u) out tab;
- exp_term e t out tab
- | D.TAppl (a, vs, t) ->
- let attrs = [X.arity (List.length vs)] in
- X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
- exp_term e t out tab
- | D.TProj (a, lenv, t) ->
- let attrs = [] in
- X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
- exp_term (D.push_proj C.start e a lenv) t out tab
- | D.TBind (a, b, t) ->
- exp_bind e a b out tab;
- exp_term (D.push_bind C.start e a b) t out tab
-
-and exp_bind e a b out tab =
- let f a ns = a, ns in
- let a, ns = Y.get_names f a in
- match b with
- | D.Abst ws ->
- let e = D.push_bind C.start e a (D.Abst []) in
- let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
- X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
- | D.Abbr vs ->
- let e = D.push_bind C.start e a (D.Abbr []) in
- let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
- X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
- | D.Void n ->
- let attrs = [X.name a; X.mark a; X.arity n] in
- X.tag X.void attrs out tab
-
-and exp_eproj e a lenv out tab =
- let attrs = [] in
- X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
-
-(****************************************************************************)
-
-let export_term = exp_term D.empty_lenv
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-val export_term: Crg.term -> Library.pp
-
val pp_term: (string -> unit) -> Crg.term -> unit
--- /dev/null
+(*
+ ||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_______________________________________________________________ *)
+
+module U = NUri
+module C = Cps
+module H = Hierarchy
+module Y = Entity
+module A = Alpha
+module X = Library
+module D = Crg
+
+(* internal functions *******************************************************)
+
+let rec list_iter map l out tab = match l with
+ | [] -> ()
+ | hd :: tl -> map hd out tab; list_iter map tl out tab
+
+let list_rev_iter map e ns l out tab =
+ let rec aux err f e = function
+ | [], [] -> f e
+ | n :: ns, hd :: tl ->
+ let f e =
+(*
+ pp_lenv print_string e; print_string " |- ";
+ pp_term print_string hd; print_newline ();
+*)
+ map e hd out tab; f (D.push2 C.err C.start e n ~t:hd ())
+ in
+ aux err f e (ns, tl)
+ | _ -> err ()
+ in
+ ignore (aux C.err C.start e (ns, l))
+
+let lenv_iter map1 map2 l out tab =
+ let rec aux f = function
+ | D.ESort -> f ()
+ | D.EBind (lenv, a, b) -> aux (fun () -> map1 a b out tab; f ()) lenv
+ | D.EProj (lenv, a, e) -> aux (fun () -> map2 a e out tab; f ()) lenv
+ in
+ aux C.start l
+
+let rec exp_term e t out tab = match t with
+ | D.TSort (a, l) ->
+ let a =
+ let err _ = a in
+ let f s = Y.Name (s, true) :: a in
+ H.string_of_sort err f l
+ in
+ let attrs = [X.position l; X.name a] in
+ X.tag X.sort attrs out tab
+ | D.TLRef (a, i, j) ->
+ let a =
+ let err _ = a in
+ let f n r = Y.Name (n, r) :: a in
+ D.get_name err f i j e
+ in
+ let attrs = [X.position i; X.offset j; X.name a] in
+ X.tag X.lref attrs out tab
+ | D.TGRef (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
+ | D.TCast (a, u, t) ->
+ let attrs = [] in
+ X.tag X.cast attrs ~contents:(exp_term e u) out tab;
+ exp_term e t out tab
+ | D.TAppl (a, vs, t) ->
+ let attrs = [X.arity (List.length vs)] in
+ X.tag X.appl attrs ~contents:(list_iter (exp_term e) vs) out tab;
+ exp_term e t out tab
+ | D.TProj (a, lenv, t) ->
+ let attrs = [] in
+ X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab;
+ exp_term (D.push_proj C.start e a lenv) t out tab
+ | D.TBind (a, b, t) ->
+(* NOTE: the inner binders are alpha-converted first *)
+(* so undesirable renamings might occur *)
+(* EX: we rename [x][x]x to [x][x_]x_ *)
+(* whereas [x_][x]x would be more desirable *)
+ let a = A.alpha (D.names_of_lenv [] e) a in
+ exp_bind e a b out tab;
+ exp_term (D.push_bind C.start e a b) t out tab
+
+and exp_bind e a b out tab =
+ let f a ns = a, ns in
+ let a, ns = Y.get_names f a in
+ match b with
+ | D.Abst ws ->
+ let e = D.push_bind C.start e a (D.Abst []) in
+ let attrs = [X.name ns; X.mark a; X.arity (List.length ws)] in
+ X.tag X.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
+ | D.Abbr vs ->
+ let e = D.push_bind C.start e a (D.Abbr []) in
+ let attrs = [X.name ns; X.mark a; X.arity (List.length vs)] in
+ X.tag X.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
+ | D.Void n ->
+ let attrs = [X.name a; X.mark a; X.arity n] in
+ X.tag X.void attrs out tab
+
+and exp_eproj e a lenv out tab =
+ let attrs = [] in
+ X.tag X.proj attrs ~contents:(lenv_iter (exp_bind e) (exp_eproj e) lenv) out tab
+
+(* interface functions ******************************************************)
+
+let export_term = exp_term D.empty_lenv
--- /dev/null
+(*
+ ||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_______________________________________________________________ *)
+
+val export_term: Crg.term -> Library.pp
| OC { block_comment lexbuf; block_comment lexbuf }
| _ { block_comment lexbuf }
and qstring = parse
- | QT { "" }
- | SPC { " " ^ qstring lexbuf }
- | BS BS { "\\" ^ qstring lexbuf }
- | BS QT { "\"" ^ qstring lexbuf }
- | _ { Lexing.lexeme lexbuf ^ qstring lexbuf }
+ | QT { "" }
+ | SPC { " " ^ qstring lexbuf }
+ | BS BS { "\\" ^ qstring lexbuf }
+ | BS QT { "\"" ^ qstring lexbuf }
+ | _ as c { String.make 1 c ^ qstring lexbuf }
and token = parse
- | SPC { token lexbuf }
- | OC { block_comment lexbuf; token lexbuf }
- | ID as id { out "ID"; P.ID id }
- | IX as ix { out "IX"; P.IX (int_of_string ix) }
- | QT { let s = qstring lexbuf in out "STR"; P.STR s }
+ | SPC { token lexbuf }
+ | OC { block_comment lexbuf; token lexbuf }
+ | ID as id { out ("ID " ^ id); P.ID id }
+ | IX as ix { out ("IX " ^ ix); P.IX (int_of_string ix) }
+ | QT { let s = qstring lexbuf in out ("STR " ^ s); P.STR s }
| "\\graph" { out "GRAPH"; P.GRAPH }
| "\\decl" { out "DECL"; P.DECL }
| "\\ax" { out "AX"; P.AX }
module MA = MetaAut
module MO = MetaOutput
module ML = MetaLibrary
-module DO = CrgOutput
+module DX = CrgXml
module DBrg = CrgBrg
module MBrg = MetaBrg
module BrgO = BrgOutput
| _ -> st
let export_entity si xdir moch = function
- | CrgEntity e -> X.export_entity DO.export_term si xdir e
+ | CrgEntity e -> X.export_entity DX.export_term si xdir e
| BrgEntity e -> X.export_entity BrgO.export_term si xdir e
| MetaEntity e ->
begin match moch with
position NMTOKEN #REQUIRED
name NMTOKENS #IMPLIED
mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT LRef EMPTY>
position NMTOKEN #REQUIRED
name NMTOKENS #IMPLIED
mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT GRef EMPTY>
uri CDATA #REQUIRED
name NMTOKENS #IMPLIED
mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT Cast %term;>
<!ATTLIST Cast
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
+ name NMTOKENS #IMPLIED
+ arity NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT Appl %term;>
<!ATTLIST Appl
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
+ name NMTOKENS #IMPLIED
+ arity NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT Abst %term;>
<!ATTLIST Abst
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
+ name NMTOKENS #IMPLIED
+ arity NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT Abbr %term;>
<!ATTLIST Abbr
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
+ name NMTOKENS #IMPLIED
+ arity NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT Void EMPTY>
<!ATTLIST Void
- name NMTOKENS #IMPLIED
- mark NMTOKENS #IMPLIED
+ name NMTOKENS #IMPLIED
+ arity NMTOKENS #IMPLIED
+ mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!-- ENVIRONMENT ENTRIES -->
uri CDATA #REQUIRED
name NMTOKENS #IMPLIED
mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!ELEMENT ABBR %term;>
uri CDATA #REQUIRED
name NMTOKENS #IMPLIED
mark NMTOKENS #IMPLIED
+ meta CDATA #IMPLIED
>
<!-- ROOT -->
projects / helm.git / commitdiff