diff options
Diffstat (limited to 'stm/texmacspp.ml')
| -rw-r--r-- | stm/texmacspp.ml | 24 |
1 files changed, 15 insertions, 9 deletions
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml index 180f20ae..b9120804 100644 --- a/stm/texmacspp.ml +++ b/stm/texmacspp.ml @@ -244,7 +244,7 @@ and pp_local_decl_expr lde = (* don't know what it is for now *) match lde with | AssumExpr (_, ce) -> pp_expr ce | DefExpr (_, ce, _) -> pp_expr ce -and pp_inductive_expr ((_, (l, id)), lbl, ceo, _, cl_or_rdexpr) = +and pp_inductive_expr ((_, ((l, id),_)), lbl, ceo, _, cl_or_rdexpr) = (* inductive_expr *) let b,e = Loc.unloc l in let location = ["begin", string_of_int b; "end", string_of_int e] in @@ -273,7 +273,7 @@ and pp_recursion_order_expr optid roe = (* don't know what it is for now *) | CMeasureRec (e, None) -> "mesrec", [pp_expr e] | CMeasureRec (e, Some rel) -> "mesrec", [pp_expr e] @ [pp_expr rel] in Element ("recursion_order", ["kind", kind] @ attrs, expr) -and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) = +and pp_fixpoint_expr (((loc, id), pl), (optid, roe), lbl, ce, ceo) = (* fixpoint_expr *) let start, stop = unlock loc in let id = Id.to_string id in @@ -286,7 +286,7 @@ and pp_fixpoint_expr ((loc, id), (optid, roe), lbl, ce, ceo) = | Some ce -> [pp_expr ce] | None -> [] end -and pp_cofixpoint_expr ((loc, id), lbl, ce, ceo) = (* cofixpoint_expr *) +and pp_cofixpoint_expr (((loc, id), pl), lbl, ce, ceo) = (* cofixpoint_expr *) (* Nota: it is like fixpoint_expr without (optid, roe) * so could be merged if there is no more differences *) let start, stop = unlock loc in @@ -473,7 +473,7 @@ and pp_expr ?(attr=[]) e = xmlApply loc (xmlOperator "fix" loc :: List.flatten (List.map - (fun (a,b,cl,c,d) -> pp_fixpoint_expr (a,b,cl,c,Some d)) + (fun (a,b,cl,c,d) -> pp_fixpoint_expr ((a,None),b,cl,c,Some d)) fel)) let pp_comment (c) = @@ -490,6 +490,9 @@ let rec tmpp v loc = | VernacTime l -> xmlApply loc (Element("time",[],[]) :: List.map (fun(loc,e) ->tmpp e loc) l) + | VernacRedirect (s, l) -> + xmlApply loc (Element("redirect",["path", s],[]) :: + List.map (fun(loc,e) ->tmpp e loc) l) | VernacTimeout (s,e) -> xmlApply loc (Element("timeout",["val",string_of_int s],[]) :: [tmpp e loc]) @@ -506,8 +509,10 @@ let rec tmpp v loc = | VernacOpenCloseScope (_,(true,name)) -> xmlScope loc "open" name [] | VernacOpenCloseScope (_,(false,name)) -> xmlScope loc "close" name [] - | VernacDelimiters (name,tag) -> + | VernacDelimiters (name,Some tag) -> xmlScope loc "delimit" name ~attr:["delimiter",tag] [] + | VernacDelimiters (name,None) -> + xmlScope loc "undelimit" name ~attr:[] [] | VernacBindScope (name,l) -> xmlScope loc "bind" name (List.map (function @@ -535,7 +540,7 @@ let rec tmpp v loc = | VernacConstraint _ | VernacPolymorphic (_, _) as x -> xmlTODO loc x (* Gallina *) - | VernacDefinition (ldk, (_,id), de) -> + | VernacDefinition (ldk, ((_,id),_), de) -> let l, dk = match ldk with | Some l, dk -> (l, dk) @@ -550,7 +555,7 @@ let rec tmpp v loc = let str_dk = Kindops.string_of_definition_kind (l, false, dk) in let str_id = Id.to_string id in (xmlDef str_dk str_id loc [pp_expr e]) - | VernacStartTheoremProof (tk, [ Some (_,id), ([], statement, None) ], b) -> + | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) -> let str_tk = Kindops.string_of_theorem_kind tk in let str_id = Id.to_string id in (xmlThm str_tk str_id loc [pp_expr statement]) @@ -570,10 +575,11 @@ let rec tmpp v loc = end | VernacExactProof _ as x -> xmlTODO loc x | VernacAssumption ((l, a), _, sbwcl) -> + let binders = List.map (fun (_, (id, c)) -> (List.map fst id, c)) sbwcl in let many = - List.length (List.flatten (List.map fst (List.map snd sbwcl))) > 1 in + List.length (List.flatten (List.map fst binders)) > 1 in let exprs = - List.flatten (List.map pp_simple_binder (List.map snd sbwcl)) in + List.flatten (List.map pp_simple_binder binders) in let l = match l with Some x -> x | None -> Decl_kinds.Global in let kind = string_of_assumption_kind l a many in xmlAssumption kind loc exprs |