From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 2 Apr 2009 14:43:52 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4122
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=718d9bcfb53dd76a5c0622aff9fed69a68769324;hp=8f4bb4db3597080b57d957eb444e58e032da2d78;p=helm.git

...
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 634ccc769..09eb2d345 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -715,9 +715,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
      prerr_endline ("nuovo lemma: " ^ NCicPp.ppmetasenv ~subst:nsubst nmenv);
      { status with
         GrafiteTypes.ng_status = 
-           GrafiteTypes.ProofMode { NTactics.gstatus = ninitial_stack; 
+           GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack; 
           istatus = { 
-            NTactics.pstatus = 
+            NTacStatus.pstatus = 
              NUri.uri_of_string suri, 0, nmenv, nsubst, 
               (NCic.Constant ([],"",Some nbo,nty,(`Provided,`Definition,`Regular)));
             lstatus = nlexicon_status} }   
@@ -820,7 +820,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status
       | GrafiteTypes.ProofMode nstatus ->
          let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in
          let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in
-         NTactics.pp_tac_status nstatus;
+         NTacStatus.pp_tac_status nstatus;
          { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, [])
   | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
      let status = 
diff --git a/helm/software/components/grafite_engine/grafiteTypes.ml b/helm/software/components/grafite_engine/grafiteTypes.ml
index 836872779..fc81efcaf 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.ml
+++ b/helm/software/components/grafite_engine/grafiteTypes.ml
@@ -45,7 +45,7 @@ type proof_status =
       * engine. No status entering/exiting the engine could be in it. *)
 
 type ng_status =
-  | ProofMode of NTactics.tac_status
+  | ProofMode of NTacStatus.tac_status
   | CommandMode of LexiconEngine.status
 
 type status = {
diff --git a/helm/software/components/grafite_engine/grafiteTypes.mli b/helm/software/components/grafite_engine/grafiteTypes.mli
index b159a7fe6..22386ebbf 100644
--- a/helm/software/components/grafite_engine/grafiteTypes.mli
+++ b/helm/software/components/grafite_engine/grafiteTypes.mli
@@ -43,7 +43,7 @@ type proof_status =
   | Intermediate of Cic.metasenv
 
 type ng_status =
-  | ProofMode of NTactics.tac_status
+  | ProofMode of NTacStatus.tac_status
   | CommandMode of LexiconEngine.status
 
 type status = {
diff --git a/helm/software/components/ng_tactics/nTacStatus.mli b/helm/software/components/ng_tactics/nTacStatus.mli
index 4ca302890..1feac415b 100644
--- a/helm/software/components/ng_tactics/nTacStatus.mli
+++ b/helm/software/components/ng_tactics/nTacStatus.mli
@@ -65,4 +65,6 @@ val select_term:
   lowtac_status -> cic_term -> ast_term option * NCic.term ->
     lowtac_status * cic_term
 
+val pp_tac_status: tac_status -> unit
+
 (* end *)
diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 128f33ac3..75c3ebafc 100644
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -73,7 +73,7 @@ let eval_ast ?do_heavy_checks lexicon_status
    | GrafiteTypes.ProofMode s -> 
       { grafite_status with GrafiteTypes.ng_status = 
          GrafiteTypes.ProofMode 
-          { s with NTactics.istatus = { s.NTactics.istatus with NTactics.lstatus =  lexicon_status }}}
+          { s with NTacStatus.istatus = { s.NTacStatus.istatus with NTacStatus.lstatus =  lexicon_status }}}
  in
  let new_grafite_status,new_objs =
   GrafiteEngine.eval_ast
@@ -87,7 +87,7 @@ let eval_ast ?do_heavy_checks lexicon_status
   else
    match new_grafite_status.GrafiteTypes.ng_status with
    | GrafiteTypes.CommandMode l -> l
-   | GrafiteTypes.ProofMode s -> s.NTactics.istatus.NTactics.lstatus
+   | GrafiteTypes.ProofMode s -> s.NTacStatus.istatus.NTacStatus.lstatus
  in
  let new_lexicon_status =
   LexiconSync.add_aliases_for_objs lexicon_status new_objs in
diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml
index df4c70ded..2d6d1cd17 100644
--- a/helm/software/matita/matitaExcPp.ml
+++ b/helm/software/matita/matitaExcPp.ml
@@ -163,6 +163,8 @@ let rec to_string =
      None, ("Disambiguation choice not found: " ^ Lazy.force msg)
   | MatitaEngine.EnrichedWithLexiconStatus (exn,_) ->
      None, "EnrichedWithLexiconStatus "^snd(to_string exn)
+  | NTacStatus.Error msg ->
+     None, "NTactic error: " ^ Lazy.force msg
   | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
      let loc =
       match errorll with