]> matita.cs.unibo.it Git - helm.git/commit
bugfix to developments:
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Jul 2006 10:40:11 +0000 (10:40 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 5 Jul 2006 10:40:11 +0000 (10:40 +0000)
commit14d7eabdb425c4dbcda5de18fac0735fde5d176b
treefebd2308433dc74747fd83d4fdca71e2c5738474
parent9571f24af9d981219cac993604997f80bb2e1b97
bugfix to developments:
- if an included .ma file is not found (not in CWD, not in include_paths)
  an error is issued
- if an included .ma file is found but the corrsponding .lexicon is not found
  a development for the .ma is searched:
  - if found it is used to compile the .ma file
  - if not found the user is aked to create a devel for the file included
    (and not the file that he is editing, that may not be in the same devel).
13 files changed:
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteEngine.mli
helm/software/components/grafite_parser/dependenciesParser.ml
helm/software/components/grafite_parser/dependenciesParser.mli
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/lexicon/lexiconAst.ml
helm/software/components/lexicon/lexiconAstPp.ml
helm/software/components/lexicon/lexiconEngine.ml
helm/software/components/lexicon/lexiconEngine.mli
helm/software/matita/matitaScript.ml
helm/software/matita/matitacLib.ml
helm/software/matita/matitaclean.ml
helm/software/matita/matitadep.ml