From 157f12c3cb9cc4ed5ba9d1e46c64a593c7fd9481 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 16 May 2005 15:21:32 +0000
Subject: [PATCH] some hacks to make the sequent window pretty nice

---
 helm/ocaml/cic_transformations/sequent2pres.ml |  3 +--
 helm/ocaml/cic_transformations/tacticAst.ml    | 11 ++++++++++-
 helm/ocaml/cic_transformations/tacticAstPp.ml  | 14 ++++++++++++++
 helm/ocaml/cic_transformations/tacticAstPp.mli |  3 +++
 4 files changed, 28 insertions(+), 3 deletions(-)

diff --git a/helm/ocaml/cic_transformations/sequent2pres.ml b/helm/ocaml/cic_transformations/sequent2pres.ml
index 24a3487b8..ad2724134 100644
--- a/helm/ocaml/cic_transformations/sequent2pres.ml
+++ b/helm/ocaml/cic_transformations/sequent2pres.ml
@@ -87,8 +87,7 @@ let sequent2pres term2pres (_,_,context,ty) =
  let pres_goal = term2pres ty in 
  (Box.b_h [] [
    Box.b_space; 
-   (Box.b_v
-      []
+   (Box.b_v []
       [Box.b_space;
        pres_context;
        b_ink [None,"width","4cm"; None,"height","2px"]; (* sequent line *)
diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index e01b7e7ed..692d4679e 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -140,11 +140,20 @@ type ('term, 'ident) tactical =
       (* try a sequence of loc * tacticals until one succeeds, fail otherwise *)
   | Try of loc * ('term, 'ident) tactical (* try a tactical and mask failures *)
 
-type ('term, 'ident) statement =
+
+type ('term, 'ident) code =
   | Command of loc * 'term command
   | Macro of loc * 'term macro 
       (* Macro are substantially queries, but since we are not the kind of
        * peolpe that like to push "start" to turn off the computer 
        * we added this command *)
   | Tactical of loc * ('term, 'ident) tactical
+             
+type ('term, 'ident) comment =
+  | Note of loc * string
+  | Code of loc * ('term, 'ident) code
+             
+type ('term, 'ident) statement =
+  | Executable of loc * ('term, 'ident) code
+  | Comment of loc * ('term, 'ident) comment
 
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index f781ea3d7..9fb8455f9 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -125,6 +125,8 @@ let pp_macro pp_term = function
   | Undo (_, Some n) -> sprintf "Undo %d" n
   | Print (_, name) -> sprintf "Print \"%s\"" name
   | Quit _ -> "Quit"
+  | Instance _
+  | Match _ -> assert false
 
 let pp_macro_ast = pp_macro pp_term_ast
 let pp_macro_cic = pp_macro pp_term_cic
@@ -198,3 +200,15 @@ and pp_tacticals tacs =
 let pp_tactical tac = pp_tactical tac ^ tactical_terminator
 let pp_tactic tac = pp_tactic tac ^ tactic_terminator
 
+let pp_executable = function
+  | Macro (_,x) -> pp_macro_ast x
+  | Tactical (_,x) -> pp_tactical x
+  | Command (_,x) -> pp_command x
+                      
+let pp_comment = function
+  | Note (_,str) -> sprintf "(* %s *)" str
+  | Code (_,code) -> sprintf "(** %s. **)" (pp_executable code)
+
+let pp_statement = function
+  | Executable (_, ex) -> pp_executable ex
+  | Comment (_, c) -> pp_comment c
diff --git a/helm/ocaml/cic_transformations/tacticAstPp.mli b/helm/ocaml/cic_transformations/tacticAstPp.mli
index f9fe2b2b8..3308adf92 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.mli
+++ b/helm/ocaml/cic_transformations/tacticAstPp.mli
@@ -26,6 +26,9 @@
 val pp_tactic: (CicAst.term, string) TacticAst.tactic -> string
 val pp_command: CicAst.term TacticAst.command -> string
 val pp_macro: ('a -> string) -> 'a TacticAst.macro -> string
+val pp_comment: (CicAst.term,string) TacticAst.comment -> string
+val pp_executable: (CicAst.term,string) TacticAst.code -> string
+val pp_statement: (CicAst.term,string) TacticAst.statement -> string
 val pp_macro_ast: CicAst.term TacticAst.macro -> string
 val pp_macro_cic: Cic.term TacticAst.macro -> string
 val pp_tactical: (CicAst.term, string) TacticAst.tactical -> string
-- 
2.39.2