applyTransformation.ml: highlevel prettyprinter disabled when reconstructing inductive types (was re-enabled by mistake)
procedural/Makefile.common: bugfix in entry names
matitaEngine: unused callback removed
lexiconAstPp: output bugfix
The first reconstructed .ma's form library now compile :)))))))
sprintf "%s%s" (Buffer.contents eta_buf) name
let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
sprintf "%s%s" (Buffer.contents eta_buf) name
let pp_interpretation dsc symbol arg_patterns cic_appl_pattern =
- sprintf "interpretation \"%s\" '%s %s = %s"
+ sprintf "interpretation \"%s\" '%s %s = %s."
dsc symbol
(String.concat " " (List.map pp_argument_pattern arg_patterns))
(CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
dsc symbol
(String.concat " " (List.map pp_argument_pattern arg_patterns))
(CicNotationPp.pp_cic_appl_pattern cic_appl_pattern)
| Some `RightToLeft -> "< "
let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
| Some `RightToLeft -> "< "
let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
- sprintf "notation %s\"%s\" %s %s for %s"
+ sprintf "notation %s\"%s\" %s %s for %s."
(pp_dir_opt dir_opt)
(pp_l1_pattern l1_pattern)
(pp_associativity assoc)
(pp_dir_opt dir_opt)
(pp_l1_pattern l1_pattern)
(pp_associativity assoc)
let pp_command = function
| Include (_,_,mode,path) -> (* not precise, since path is absolute *)
if mode = WithPreferences then
let pp_command = function
| Include (_,_,mode,path) -> (* not precise, since path is absolute *)
if mode = WithPreferences then
- "include \"" ^ path ^ "\".\n"
+ "include \"" ^ path ^ "\"."
- "include' \"" ^ path ^ "\".\n"
+ "include' \"" ^ path ^ "\"."
| Alias (_,s) -> pp_alias s
| Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
pp_interpretation dsc symbol arg_patterns cic_appl_pattern
| Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
pp_notation dir_opt l1_pattern assoc prec l2_pattern
| Alias (_,s) -> pp_alias s
| Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
pp_interpretation dsc symbol arg_patterns cic_appl_pattern
| Notation (_, dir_opt, l1_pattern, assoc, prec, l2_pattern) ->
pp_notation dir_opt l1_pattern assoc prec l2_pattern
let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
remove_closed_substs s
let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
remove_closed_substs s
-let enable_notations x = () (* function
+let enable_notations = function
| true ->
CicNotation.set_active_notations
(List.map fst (CicNotation.get_all_notations ()))
| false ->
CicNotation.set_active_notations []
| true ->
CicNotation.set_active_notations
(List.map fst (CicNotation.get_all_notations ()))
| false ->
CicNotation.set_active_notations []
let txt_of_cic_object
~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas
n style ?flavour prefix obj
let txt_of_cic_object
~map_unicode_to_tex ?skip_thm_and_qed ?skip_initial_lambdas
n style ?flavour prefix obj
$(H)$(RM) $(LOG)
$(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG)
$(H)$(RM) $(LOG)
$(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG)
- $(H)$(BIN)matitac $(MATITAOPTIONS) $@ 2>> $(LOG)
-%.ma.opt:
+ $(H)$(BIN)matitac $(MATITAOPTIONS) $*.mma 2>> $(LOG)
+%.mo:
- $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.ma 2>> $(LOG)
-%.mma.opt:
+ $(H)$(BIN)matitac $(MATITAOPTIONS) $*.ma 2>> $(LOG)
+%.ma.opt:
$(H)$(RM) $(LOG)
$(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.mma 2>> $(LOG)
$(H)$(RM) $(LOG)
$(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.mma 2>> $(LOG)
+%.mo.opt:
+ $(H)$(RM) $(LOG)
+ $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.ma 2>> $(LOG)
clean:
$(H)$(BIN)matitaclean $(MATITAOPTIONS)
clean:
$(H)$(BIN)matitaclean $(MATITAOPTIONS)
exception TryingToAdd of string
exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status
exception TryingToAdd of string
exception EnrichedWithStatus of exn * LexiconEngine.status * GrafiteTypes.status
-let out = ref ignore
-
-let set_callback f = out := f
-
let eval_from_stream ~first_statement_only ~include_paths
?do_heavy_checks ?(enforce_no_new_aliases=true)
?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb
let eval_from_stream ~first_statement_only ~include_paths
?do_heavy_checks ?(enforce_no_new_aliases=true)
?(watch_statuses=fun _ _ -> ()) lexicon_status grafite_status str cb
false, lexicon_status, grafite_status,
(((grafite_status,lexicon_status),None)::statuses)
| GrafiteParser.LSome ast ->
false, lexicon_status, grafite_status,
(((grafite_status,lexicon_status),None)::statuses)
| GrafiteParser.LSome ast ->
cb grafite_status ast;
let new_statuses =
eval_ast ?do_heavy_checks lexicon_status
cb grafite_status ast;
let new_statuses =
eval_ast ?do_heavy_checks lexicon_status
GrafiteAst.statement -> unit) ->
((GrafiteTypes.status * LexiconEngine.status) *
(DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
GrafiteAst.statement -> unit) ->
((GrafiteTypes.status * LexiconEngine.status) *
(DisambiguateTypes.domain_item * LexiconAst.alias_spec) option) list
-
-(* this callback is called on every grafite command *)
-val set_callback: (GrafiteParser.ast_statement -> unit) -> unit
exception AttemptToInsertAnAlias of LexiconEngine.status
exception AttemptToInsertAnAlias of LexiconEngine.status
-let out = ref ignore
-let set_callback f = out := f
-
-
let slash_n_RE = Pcre.regexp "\\n" ;;
let pp_ast_statement grafite_status stm =
let slash_n_RE = Pcre.regexp "\\n" ;;
let pp_ast_statement grafite_status stm =
let module G = GrafiteAst in
let module L = LexiconAst in
let module H = HExtlib in
let module G = GrafiteAst in
let module L = LexiconAst in
let module H = HExtlib in
- Helm_registry.set_bool "matita.moo" false;
let floc = H.dummy_floc in
let nl_ast = G.Comment (floc, G.Note (floc, "")) in
let pp_statement stm =
let floc = H.dummy_floc in
let nl_ast = G.Comment (floc, G.Note (floc, "")) in
let pp_statement stm =
let nl () = output_string och (pp_statement nl_ast) in
MatitaMisc.out_preamble och;
let grafite_parser_cb status = function
let nl () = output_string och (pp_statement nl_ast) in
MatitaMisc.out_preamble och;
let grafite_parser_cb status = function
- | G.Executable (_, G.Macro (_, G.Inline _)) -> ()
- | stm ->
+ | G.Executable (_, G.Macro (_, G.Inline (_, style, uri, prefix, flavour))) ->
+ let str =
+ ApplyTransformation.txt_of_inline_macro style prefix uri
+ ?flavour
+ ~map_unicode_to_tex:
+ (Helm_registry.get_bool "matita.paste_unicode_as_tex")
+ in
+ output_string och str
+ | stm ->
output_string och (pp_statement stm); nl (); nl ()
in
let lexicon_parser_cb status cmd =
output_string och (pp_lexicon cmd); nl (); nl ()
in
output_string och (pp_statement stm); nl (); nl ()
in
let lexicon_parser_cb status cmd =
output_string och (pp_lexicon cmd); nl (); nl ()
in
-(*
- let matita_engine_cb = function
- | G.Executable (_, G.Macro (_, G.Inline _))
- | G.Executable (_, G.Command (_, G.Include _)) -> ()
- | ast ->
-*)
- let matitac_lib_cb = output_string och in
+ Helm_registry.set_bool "matita.moo" false;
GrafiteParser.set_grafite_callback grafite_parser_cb;
GrafiteParser.set_grafite_callback grafite_parser_cb;
- GrafiteParser.set_lexicon_callback lexicon_parser_cb;
-(*
- MatitaEngine.set_callback matita_engine_cb;
-*)
- set_callback matitac_lib_cb
+ GrafiteParser.set_lexicon_callback lexicon_parser_cb
end,
begin fun x ->
close_out och;
GrafiteParser.set_grafite_callback (fun _ _ -> ());
GrafiteParser.set_lexicon_callback (fun _ _ -> ());
end,
begin fun x ->
close_out och;
GrafiteParser.set_grafite_callback (fun _ _ -> ());
GrafiteParser.set_lexicon_callback (fun _ _ -> ());
+ Helm_registry.set_bool "matita.moo" true;
+ x
| [] -> lexicon_status, grafite_status
| ((grafite,lexicon),None)::_ -> lexicon, grafite
| ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
| [] -> lexicon_status, grafite_status
| ((grafite,lexicon),None)::_ -> lexicon, grafite
| ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l)
with MatitaEngine.EnrichedWithStatus
(GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn ->
match f (get_macro_context (Some grafite)) with
| _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
with MatitaEngine.EnrichedWithStatus
(GrafiteEngine.Macro (floc, f), lexicon, grafite) as exn ->
match f (get_macro_context (Some grafite)) with
| _, GrafiteAst.Inline (_, style, suri, prefix, flavour) ->
ApplyTransformation.txt_of_inline_macro style prefix suri
?flavour
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
in
!out str;
ApplyTransformation.txt_of_inline_macro style prefix suri
?flavour
~map_unicode_to_tex:(Helm_registry.get_bool
"matita.paste_unicode_as_tex")
in
!out str;
aux_for_dump x lexicon grafite
|_-> raise exn
in
aux_for_dump x lexicon grafite
|_-> raise exn
in
*)
clean_exit baseuri false)
else
*)
clean_exit baseuri false)
else
- (if not (Helm_registry.get_bool "matita.moo" &&
- Filename.check_suffix fname ".mma") then begin
+ (if Helm_registry.get_bool "matita.moo" then begin
(* FG: we do not generate .moo when dumping .mma files *)
GrafiteMarshal.save_moo moo_fname moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
(* FG: we do not generate .moo when dumping .mma files *)
GrafiteMarshal.save_moo moo_fname moo_content_rev;
LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;