added contextual menu to act over selected terms

[helm.git] / helm / matita / matitaScript.ml

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index c14bd77101628212a200e1066d31252c9c9792b5..a545b65d492cb4b65fc0cfaba8985a06ceeb3900 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -229,6 +229,10 @@ let disambiguate_macro_term term status user_goal =
   match interps with 
   | [_,_,x,_], _ -> x
   | _ -> assert false
+
+let pp_eager_statement_ast =
+  GrafiteAstPp.pp_statement ~term_pp:CicNotationPp.pp_term
+    ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
  
 let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   let module TAPp = GrafiteAstPp in
@@ -239,6 +243,8 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   (* no idea why ocaml wants this *)
   let parsed_text_length = String.length parsed_text in
   let dbd = LibraryDb.instance () in
+  (* XXX use a real CIC -> string pretty printer *)
+  let pp_macro = TAPp.pp_macro ~term_pp:CicPp.ppterm in
   match mac with
   (* WHELP's stuff *)
   | TA.WMatch (loc, term) -> 
@@ -254,12 +260,12 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
   | TA.WInstance (loc, term) ->
       let term = disambiguate_macro_term term status user_goal in
       let l = Whelp.instance ~dbd term in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WInstance (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WLocate (loc, s) -> 
       let l = Whelp.locate ~dbd s in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in
+      let entry = `Whelp (pp_macro (TA.WLocate (loc, s)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WElim (loc, term) ->
@@ -270,14 +276,14 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
         | _ -> failwith "Not a MutInd"
       in
       let l = Whelp.elim ~dbd uri in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WElim (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   | TA.WHint (loc, term) ->
       let term = disambiguate_macro_term term status user_goal in
       let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in
       let l = List.map fst (MQ.experimental_hint ~dbd s) in
-      let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in
+      let entry = `Whelp (pp_macro (TA.WHint (loc, term)), l) in
       guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
       [], parsed_text_length
   (* REAL macro *)
@@ -303,9 +309,7 @@ let eval_macro guistuff status user_goal unparsed_text parsed_text script mac =
           ~disambiguate_command:GrafiteDisambiguate.disambiguate_command
           status ast in
         let extra_text = 
-          comment parsed_text ^ 
-          "\n" ^ TAPp.pp_statement ast
-        in
+          comment parsed_text ^ "\n" ^ pp_eager_statement_ast ast in
         [ new_status , (extra_text, ast) ], parsed_text_length
       | _ -> 
           HLog.error