From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Tue, 20 Mar 2012 16:27:14 +0000 (+0000)
Subject: Matitaweb:
X-Git-Tag: make_still_working~1843
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3800a841aa7115b10432f588d31b77129b3a0dc9

Matitaweb:
1) partially solves a problem with TeX-like macro conversion when the script contains markup
2) ports a bugfix from Matita 1.0 (see log for revision 11211).
---

diff --git a/matitaB/components/grafite_parser/grafiteParser.ml b/matitaB/components/grafite_parser/grafiteParser.ml
index 7985512d9..a63206994 100644
--- a/matitaB/components/grafite_parser/grafiteParser.ml
+++ b/matitaB/components/grafite_parser/grafiteParser.ml
@@ -42,15 +42,17 @@ let exc_located_wrapper f =
       raise (HExtlib.Localized 
         (floc,CicNotationParser.Parse_error (Printexc.to_string exn)))
 
-type parsable = Grammar.parsable
+type parsable = Grammar.parsable * Ulexing.lexbuf
 
 let parsable_statement status buf =
  let grammar = CicNotationParser.level2_ast_grammar status in
-  Grammar.parsable grammar (Obj.magic buf)
+  Grammar.parsable grammar (Obj.magic buf), buf
 
 let parse_statement grafite_parser parsable =
   exc_located_wrapper
-    (fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) parsable))
+    (fun () -> (Grammar.Entry.parse_parsable (Obj.magic grafite_parser) (fst parsable)))
+
+let strm_of_parsable (_,buf) = buf
 
 let add_raw_attribute ~text t = N.AttributedTerm (`Raw text, t)
 
diff --git a/matitaB/components/grafite_parser/grafiteParser.mli b/matitaB/components/grafite_parser/grafiteParser.mli
index 4f3ce988e..9e6f1dc6f 100644
--- a/matitaB/components/grafite_parser/grafiteParser.mli
+++ b/matitaB/components/grafite_parser/grafiteParser.mli
@@ -51,3 +51,4 @@ val extend : #status as 'status ->
 type parsable
 val parsable_statement: #status -> Ulexing.lexbuf -> parsable
 val parse_statement: #status -> parsable -> GrafiteAst.statement
+val strm_of_parsable: parsable -> Ulexing.lexbuf
diff --git a/matitaB/matita/html/matitaweb.js b/matitaB/matita/html/matitaweb.js
index d367b6bb3..cec0bb3ba 100644
--- a/matitaB/matita/html/matitaweb.js
+++ b/matitaB/matita/html/matitaweb.js
@@ -211,10 +211,10 @@ function lookup_tex(texmacro)
 function strip_tags(tagname,classname) 
 {
     var tags = unlocked.getElementsByTagName(tagname);
-    var tlen = tags.length; // preserving the value from removeChild operations
     if (is_defined(classname)) {
 	tags = filterByClass(tags,classname);
     }
+    var tlen = tags.length; // preserving the value from removeChild operations
     for (i = 0; i < tlen; i++) {
         var children = tags[i].childNodes;
         for (j = 0; j < children.length; j++) {
diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 14716e2b6..734140ad3 100644
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -147,28 +147,37 @@ let rec get_ast status ~compiling ~asserted ~include_paths strm =
 
 and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status str cb =
  let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop asserted status =
-  let asserted,stop,status = 
+ let rec loop asserted status str =
+  let asserted,stop,status,str = 
    try
      let cont =
        try Some (get_ast status ~compiling ~asserted ~include_paths str)
        with End_of_file -> None in
      match cont with
-     | None -> asserted, true, status
+     | None -> asserted, true, status, str
      | Some (asserted,ast) ->
         (* pp_ast_statement status ast; *)
         cb status ast;
         let status =
           eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
         in
-         asserted, false, status
+        let str =
+         match ast with
+            (GrafiteAst.Executable
+              (_,GrafiteAst.NCommand
+                (_,(GrafiteAst.Include _ | GrafiteAst.Notation _)))) ->
+              GrafiteParser.parsable_statement status
+               (GrafiteParser.strm_of_parsable str)
+          | _ -> str
+        in
+         asserted, false, status, str
    with exn when not matita_debug ->
      prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn);
      raise (EnrichedWithStatus (exn, status))
   in
-  if stop then asserted,status else loop asserted status
+  if stop then asserted,status else loop asserted status str
  in
-  loop asserted status
+  loop asserted status str
 
 and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
   if List.mem fname compiling then raise (CircularDependency fname);