basic support for imposed flavour in procedural object rendering

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index ae9aa50270319ef2cedf6eee81c6e995633f1ede..df436e7097cefe67fb842f59414a9f3258ad6b12 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -114,6 +114,7 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   (* First order tactics *)
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
+  | ApplyP (_, term) -> "applyP " ^ term_pp term
   | ApplyS (_, term, params) ->
      "applyS " ^ term_pp term ^ pp_auto_params ~term_pp params
   | AutoBatch (_,params) -> "autobatch " ^ 
@@ -257,6 +258,17 @@ let pp_macro ~term_pp =
   let prefix_pp prefix = 
      if prefix = "" then "" else Printf.sprintf " \"%s\"" prefix
   in
+  let flavour_pp = function
+     | None                   -> ""
+     | Some `Definition       -> "as definition"
+     | Some `MutualDefinition -> "as mutual"
+     | Some `Fact             -> "as fact"
+     | Some `Lemma            -> "as lemma"
+     | Some `Remark           -> "as remark"
+     | Some `Theorem          -> "as theorem"
+     | Some `Variant          -> "as variant"
+     | Some `Axiom            -> "as axiom"
+  in
   function 
   (* Whelp *)
   | WInstance (_, term) -> "whelp instance " ^ term_pp term
@@ -269,8 +281,8 @@ let pp_macro ~term_pp =
   | Hint (_, true) -> "hint rewrite"
   | Hint (_, false) -> "hint"
   | AutoInteractive (_,params) -> "auto " ^ pp_auto_params ~term_pp params
-  | Inline (_, style, suri, prefix) ->  
-      Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix) 
+  | Inline (_, style, suri, prefix, flavour) ->  
+      Printf.sprintf "inline %s\"%s\"%s%s" (style_pp style) suri (prefix_pp prefix) (flavour_pp flavour) 
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"