Partially working table layout of matita web (only on some browsers).

[helm.git] / matitaB / matita / matitaEngine.ml

diff --git a/matitaB/matita/matitaEngine.ml b/matitaB/matita/matitaEngine.ml
index 913ba87f6a835e8269bdd3973297ed7b81ddff03..437121b73f9aed171ba0184763b2d810ba1a7773 100644 (file)
--- a/matitaB/matita/matitaEngine.ml
+++ b/matitaB/matita/matitaEngine.ml
@@ -116,36 +116,9 @@ let activate_extraction baseuri fname =
 ;;
 
 
-let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) =
+let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast as ast') =
  let baseuri = status#baseuri in
- let new_aliases,new_status =
-  GrafiteDisambiguate.eval_with_new_aliases status
-   (fun status ->
-     GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status
-      (text,prefix_len,ast)) in
- let _,intermediate_states = 
-  List.fold_left
-   (fun (status,acc) (k,value) -> 
-     let v = GrafiteAst.description_of_alias value in
-     let b =
-      try
-       let NReference.Ref (uri,_) = NReference.reference_of_string v in
-        NUri.baseuri_of_uri uri = baseuri
-      with
-       NReference.IllFormedReference _ ->
-        false (* v is a description, not a URI *)
-     in
-      if b then 
-       status,acc
-      else
-       let status =
-        GrafiteDisambiguate.set_proof_aliases status ~implicit_aliases:false
-         GrafiteAst.WithPreferences [k,value]
-       in
-        status, (status ,Some (k,value))::acc
-   ) (status,[]) new_aliases (* WARNING: this must be the old status! *)
- in
-  (new_status,None)::intermediate_states
+   GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status ast'
 ;;
 
 let baseuri_of_script ~include_paths fname =
@@ -184,14 +157,8 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
      | None -> asserted, true, status
      | Some (asserted,ast) ->
         cb status ast;
-        let new_statuses =
-          eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
         let status =
-         match new_statuses with
-            [s,None] -> s
-          | _::(_,Some (_,value))::_ ->
-                raise (TryingToAdd (lazy (GrafiteAstPp.pp_alias value)))
-          | _ -> assert false
+          eval_ast ~include_paths ?do_heavy_checks status ("",0,ast)
         in
          asserted, false, status
    with exn when not matita_debug ->
@@ -201,7 +168,7 @@ and eval_from_stream ~compiling ~asserted ~include_paths ?do_heavy_checks status
  in
   loop asserted status
 
-and compile ~compiling ~asserted ~include_paths fname =
+and compile ~compiling ~asserted ~include_paths ~outch fname =
   if List.mem fname compiling then raise (CircularDependency fname);
   let compiling = fname::compiling in
   let matita_debug = Helm_registry.get_bool "matita.debug" in
@@ -269,6 +236,10 @@ and compile ~compiling ~asserted ~include_paths fname =
      HLog.message 
        (sprintf "execution of %s completed in %s." fname (hou^min^sec));
      pp_times fname true big_bang big_bang_u big_bang_s;
+     (* XXX: update script -- currently to stdout *)
+     let origbuf = Ulexing.from_utf8_channel (open_in fname) in
+     let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
+     ignore (SmallLexer.mk_small_printer interpr outch origbuf);
      asserted
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
      LexiconSync.time_travel 
@@ -276,14 +247,14 @@ and compile ~compiling ~asserted ~include_paths fname =
 *))
   with 
   (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
-  | exn when not matita_debug ->
+  | exn when not matita_debug -> 
 (* MATITA 1.0: debbo fare time_travel sulla ng_library?
        LexiconSync.time_travel ~present:lexicon ~past:initial_lexicon_status;
  *       *)
       pp_times fname false big_bang big_bang_u big_bang_s;
       clean_exit baseuri exn
 
-and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
+and assert_ng ~already_included ~compiling ~asserted ~include_paths ?outch mapath =
  let _,baseuri,fullmapath,_ = Librarian.baseuri_of_script ~include_paths mapath in
  if List.mem fullmapath asserted then asserted,false
  else
@@ -328,13 +299,19 @@ and assert_ng ~already_included ~compiling ~asserted ~include_paths mapath =
        (* maybe recompiling it I would get the same... *)
        raise (AlreadyLoaded (lazy mapath))
      else
-      let asserted = compile ~compiling ~asserted ~include_paths fullmapath in
+      let outch, is_file_ch = 
+        match outch with
+        | None -> open_out (fullmapath ^ ".mad"), true
+        | Some c -> c, false
+      in
+      let asserted = compile ~compiling ~asserted ~include_paths ~outch fullmapath in
+       if is_file_ch then close_out outch;
        fullmapath::asserted,true
   end
 ;;
 
-let assert_ng ~include_paths mapath =
+let assert_ng ~include_paths ?outch mapath =
  snd (assert_ng ~include_paths ~already_included:[] ~compiling:[] ~asserted:[]
-  mapath)
+  ?outch mapath)
 let get_ast status ~include_paths strm =
  snd (get_ast status ~compiling:[] ~asserted:[] ~include_paths strm)