From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 22 Jun 2008 15:13:14 +0000 (+0000)
Subject: - grafiteParser.ml: the callback invocation was displaced
X-Git-Tag: make_still_working~5003
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63ed9d3148199584ae8b238f018e0f9883768ada;p=helm.git

- grafiteParser.ml: the callback invocation was displaced
- cicNotationPres.ml: hack to have more brackets because
  (forall .. \to ..) was rendered without brackets. FIXME!
- LAMBDA-TYPES: improved Makefile
---

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 84eaaeb2a..175aae993 100644
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -188,7 +188,8 @@ let add_parens child_prec curr_prec t =
     child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos)
     curr_prec; *)
   if is_atomic t then t
-  else if child_prec >= 0 && child_prec < curr_prec then 
+(* FG: FIXME: should be < but < causes no brackets when \forall .. \to .. associates to the left *)  
+  else if child_prec >= 0 && child_prec <= curr_prec then 
     begin (* parens should be added *)
 (*      prerr_endline "adding parens!";  *)
     match t with
diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 18c30d4ec..20aad1cd3 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -711,6 +711,7 @@ EXTEND
     | com = comment ->
        fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
+       !out fname;       
        fun ?(never_include=false) ~include_paths status ->
         let _root, buri, fullpath, _rrelpath = 
           Librarian.baseuri_of_script ~include_paths fname 
@@ -720,7 +721,6 @@ EXTEND
          else LexiconEngine.eval_command status 
                 (LexiconAst.Include (iloc,buri,mode,fullpath))
         in
-         !out fname;
          status,
           LSome
           (GrafiteAst.Executable
diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
index fb55d6782..9608434b6 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
@@ -6,27 +6,31 @@ MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass
 
 DIR=$(shell basename $$PWD)
 
+LOG = log.txt
+
 MMAS = $(shell find Legacy-2 Base-2 -name "*.mma") 
 MAS = $(MMAS:%.mma=%.ma)
 XMAS = Legacy-2/theory.ma Base-2/theory.ma LambdaDelta-2/theory.ma
 
 $(DIR) all: depends
+	$(H)$(RM) $(LOG)
 	$(H)$(MAKE) H=$(H) --no-print-directory build
 
 $(DIR).opt opt all.opt: depends
+	$(H)$(RM) $(LOG)
 	$(H)$(MAKE) H=$(H) --no-print-directory build.opt
 
 build: $(MAS)
 	$(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends
 	$(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends
-	$(H)$(BIN)matitac $(MATITAOPTIONS) 2> /dev/null
-	$(H)rm depends
+	$(H)$(BIN)matitac $(MATITAOPTIONS) 2>> $(LOG)
+	$(H)$(RM) depends
 
 build.opt: $(MAS)
 	$(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends
 	$(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends
-	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2> /dev/null
-	$(H)rm depends
+	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG)
+	$(H)$(RM) depends
 
 clean:
 	$(H)$(BIN)matitaclean $(MATITAOPTIONS)
@@ -53,8 +57,8 @@ depend.opt:
 depends: depend.opt
 
 %.ma: %.mma
-	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) $(word 3,$(shell grep -h $< */depends)) `$(BIN)matitadep.opt -stdout $<` 2> /dev/null
-	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) -dump $@ $< 2> /dev/null
+	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) $(word 3,$(shell grep -h $< */depends)) `$(BIN)matitadep.opt -stdout $<` 2>> $(LOG)
+	$(H)$(BIN)matitac.opt $(MATITAOPTIONS) -dump $@ $< 2>> $(LOG)
 	$(H)echo $@ `$(BIN)matitadep.opt -stdout $@` >> depends
 
 include Legacy-2/.depend