Improved support for notations enriched with hyperlinks.
This revision introduces a "ref" keyword which can be used in the lefthand side
of notation statements. "ref" can only be used to decorate literals (i.e.
symbols, numbers, or keywords). The syntax is as follows:
LITERAL ::= SIMPLE_LITERAL
| ref CSYMBOL SIMPLE_LITERAL
For example, the notation
ref 'cons [ list0 x sep ; ref 'nil ]
used as the compact notation for lists specifies that the `[' symbol will be
enriched with the interpretation of 'cons nodes of the AST, and the `]' symbol
with the interpretation of 'nil nodes of the AST.
| NumValue of string
| OptValue of value option
| ListValue of value list
- | DisambiguationValue of (Stdpp.location * string option * string option)
+ (* optional name of Ast.Symbols that we want to contain the interpretation of this literal
+ * location of the literal we are parsing
+ * optional uri, optional desc *)
+ | DisambiguationValue of (string option * Stdpp.location * string option * string option)
type value_type =
| TermType of int (* the level of the expected term *)
| NumValue of string
| OptValue of value option
| ListValue of value list
- | DisambiguationValue of (Stdpp.location * string option * string option)
+ | DisambiguationValue of (string option * Stdpp.location * string option * string option)
type value_type =
| TermType of int (* the level of the expected term *)
| `Exists -> "exists"
| `Forall -> "forall"
-let pp_literal =
+(* XXX: ignoring the optional CSYMBOL
+ * (it's fine if this is only used for pretty printing output notations) *)
+let pp_literal (_,t) =
if debug_printing then
- (function (* debugging version *)
- | `Symbol _ as t ->
+ (match t with (* debugging version *)
+ | `Symbol _ ->
sprintf "symbol(%s)" (NotationUtil.string_of_literal t)
- | `Keyword _ as t ->
+ | `Keyword _ ->
sprintf "keyword(%s)" (NotationUtil.string_of_literal t)
- | `Number _ as t -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
- else NotationUtil.string_of_literal
+ | `Number _ -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
+ else NotationUtil.string_of_literal t
let pp_pos =
function
and pp_sep_opt = function
| None -> ""
- | Some sep -> sprintf " sep %s" (pp_literal sep)
+ | Some sep -> sprintf " sep %s" (pp_literal (None,sep))
and pp_variable = function
| Ast.NumVar s -> "number " ^ s
(** To be increased each time the term type below changes, used for "safe"
* marshalling *)
-let magic = 7
+let magic = 8
type term =
(* CIC AST *)
| NCic of NCic.term
(* Syntax pattern extensions *)
-
- | Literal of literal
+ (* string option = optional name of an Ast.Symbol occurring in the level 2
+ * term, which is associated to this literal *)
+ | Literal of (string option * literal)
| Layout of layout_pattern
| Magic of magic_term
let rec aux = function
| Ast.AttributedTerm (_, t) -> aux t
| Ast.Layout l -> Ast.Layout (visit_layout aux l)
- | Ast.Literal (`Keyword (k,_)) as t ->
+ | Ast.Literal (_,`Keyword (k,_)) as t ->
add_keyword k;
t
| Ast.Literal _ as t -> t
let rec get_idrefs =
function
- | Ast.Symbol (_,Some (_,desc)) -> [desc]
+ | Ast.Symbol (csym,Some (uri,desc)) -> [csym,uri,desc]
| _ -> []
let meta_names_of_term term =
val strip_attributes: NotationPt.term -> NotationPt.term
(** @return the list of proper (i.e. non recursive) IdRef of a term *)
-val get_idrefs: NotationPt.term -> string list
+val get_idrefs: NotationPt.term -> (string * string option * string) list
(** generalization of List.combine to n lists *)
val ncombine: 'a list list -> 'a list list
"break";
"list0"; "list1"; "sep";
"opt";
- "term"; "ident"; "number";
+ "term"; "ident"; "number"; "ref"
] @ level1_layouts
let level2_meta_keywords =
- [ "if"; "then"; "elCicNotationParser.se";
+ [ "if"; "then"; "else";
"fold"; "left"; "right"; "rec";
"fail";
"default";
lexer
| utf8_blank+ -> ligatures_token level1_pattern_token lexbuf
| number -> return lexbuf ("NUMBER", Ulexing.utf8_lexeme lexbuf)
- | hreftag -> return lexbuf ("ATAG", "")
+(* | hreftag -> return lexbuf ("ATAG", "")
| hrefclose -> return lexbuf ("ATAGEND","")
| generictag
- | closetag -> ligatures_token level1_pattern_token lexbuf
+ | closetag -> ligatures_token level1_pattern_token lexbuf *)
+ | qkeyword ->
+ return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))
+ | csymbol -> prerr_endline ("lexing csymbol " ^ (Ulexing.utf8_lexeme lexbuf));
+ return lexbuf ("CSYMBOL", remove_left_quote (Ulexing.utf8_lexeme lexbuf))
| ident -> handle_keywords lexbuf (fun x -> List.mem x level1_keywords) "IDENT"
| variable_ident -> return lexbuf ("IDENT", Ulexing.utf8_lexeme lexbuf)
| pident-> handle_keywords lexbuf (fun x->List.mem x level1_keywords) "PIDENT"
| floatwithunit ->
return lexbuf ("FLOATWITHUNIT", Ulexing.utf8_lexeme lexbuf)
| tex_token -> return lexbuf (expand_macro lexbuf)
- | qkeyword ->
- return lexbuf ("QKEYWORD", remove_quotes (Ulexing.utf8_lexeme lexbuf))
| '(' -> return lexbuf ("LPAREN", "")
| ')' -> return lexbuf ("RPAREN", "")
| eof -> return_eoi lexbuf
~refresh_uri_in_reference t, n)
type binding =
- | NoBinding
+ | NoBinding of string option (* name of Ast.Symbol associated to this literal *)
| Binding of string * Env.value_type
| Env of (string * Env.value_type) list
let rec aux (vl : NotationEnv.t) =
function
[] -> Gramext.action (fun (loc: Ast.location) -> action vl loc)
- | NoBinding :: tl ->
+ | NoBinding csym :: tl ->
Gramext.action
(fun ((*_,*)(loc: Ast.location)) ->
let uri,desc =
try
+ let a,b = HExtlib.loc_of_floc loc in
CicNotationLexer.LocalizeEnv.find loc
!(status#notation_parser_db.loctable)
with Not_found -> None, None
in aux (("",(Env.NoType,
- Env.DisambiguationValue (loc,uri,desc)))::vl) tl)
+ Env.DisambiguationValue (csym,loc,uri,desc)))::vl) tl)
(* LUCA: DEFCON 3 BEGIN *)
| Binding (name, Env.TermType l) :: tl ->
Gramext.action
let rec aux acc =
function
[] -> List.rev acc
- | NoBinding :: tl -> aux acc tl
+ | NoBinding _ :: tl -> aux acc tl
| Env names :: tl -> aux (List.rev names @ acc) tl
| Binding (name, ty) :: tl -> aux ((name, ty) :: acc) tl
in
assert false
and aux_literal status =
function
- | `Symbol (s,_) -> add_item_to_grammar status (`Sym s)
- | `Keyword (s,_) ->
+ | _,`Symbol (s,_) -> add_item_to_grammar status (`Sym s)
+ | _,`Keyword (s,_) ->
if not (List.mem s CicNotationLexer.initial_keywords)
then add_item_to_grammar status (`Kwd s)
else status
- | `Number _ -> status
+ | _,`Number _ -> status
and aux_layout status = function
| Ast.Sub (p1, p2) -> aux (aux status p1) p2
| Ast.Sup (p1, p2) -> aux (aux status p1) p2
| Ast.List0 (p, s)
| Ast.List1 (p, s) ->
let status =
- match s with None -> status | Some s' -> aux_literal status s'
+ match s with None -> status | Some s' -> aux_literal status (None,s')
in
aux status p
| _ -> assert false
assert false
and aux_literal =
function
- | `Symbol (s,_) -> [NoBinding, gram_symbol status s]
- | `Keyword (s,_) ->
+ | csym,`Symbol (s,_) -> [NoBinding csym, gram_symbol status s]
+ | csym,`Keyword (s,_) ->
(* assumption: s will be registered as a keyword with the lexer *)
- [NoBinding, gram_keyword status s]
- | `Number (s,_) -> [NoBinding, gram_number s]
+ [NoBinding csym, gram_keyword status s]
+ | csym,`Number (s,_) -> [NoBinding csym, gram_number s]
and aux_layout = function
- | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sub "] @ aux p2
- | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\sup "] @ aux p2
- | Ast.Below (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\below "] @ aux p2
- | Ast.Above (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\above "] @ aux p2
- | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\frac "] @ aux p2
- | Ast.InfRule (p1, p2, p3) -> [NoBinding, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
- | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\atop "] @ aux p2
- | Ast.Over (p1, p2) -> aux p1 @ [NoBinding, gram_symbol status "\\over "] @ aux p2
+ | Ast.Sub (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sub "] @ aux p2
+ | Ast.Sup (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\sup "] @ aux p2
+ | Ast.Below (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\below "] @ aux p2
+ | Ast.Above (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\above "] @ aux p2
+ | Ast.Frac (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\frac "] @ aux p2
+ | Ast.InfRule (p1, p2, p3) -> [NoBinding None, gram_symbol status "\\infrule "] @ aux p1 @ aux p2 @ aux p3
+ | Ast.Atop (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\atop "] @ aux p2
+ | Ast.Over (p1, p2) -> aux p1 @ [NoBinding None, gram_symbol status "\\over "] @ aux p2
| Ast.Root (p1, p2) ->
- [NoBinding, gram_symbol status "\\root "] @ aux p2
- @ [NoBinding, gram_symbol status "\\of "] @ aux p1
- | Ast.Sqrt p -> [NoBinding, gram_symbol status "\\sqrt "] @ aux p
+ [NoBinding None, gram_symbol status "\\root "] @ aux p2
+ @ [NoBinding None, gram_symbol status "\\of "] @ aux p1
+ | Ast.Sqrt p -> [NoBinding None, gram_symbol status "\\sqrt "] @ aux p
| Ast.Break -> []
| Ast.Box (_, pl) -> List.flatten (List.map aux pl)
| Ast.Group pl -> List.flatten (List.map aux pl)
| n = NUMBER -> `Number (n,(None,None))
]
];
+ rliteral: [
+ [ csymname = OPT [ "ref" ; csymname = CSYMBOL ->
+ prerr_endline ("parser in rliteral (ref " ^ csymname ^ ")");
+ csymname ];
+ lit = literal ->
+ csymname, lit
+ ]
+ ];
sep: [ [ "sep"; sep = literal -> sep ] ];
l1_magic_pattern: [
[ "list0"; p = l1_simple_pattern; sep = OPT sep ->
return_term_of_level loc (fun l -> Ast.Magic (m l))
| v = l1_pattern_variable ->
return_term_of_level loc (fun _ -> Ast.Variable v)
- | l = literal -> return_term_of_level loc (fun _ -> Ast.Literal l)
+ | l = rliteral -> return_term_of_level loc (fun _ -> Ast.Literal l)
]
];
END
Box.H ([],
(Box.Text ([], "?"^string_of_int n)::
(if (l <> []) then [Box.H ([],local_context)] else [])))
- | A.Literal (`Symbol (s,x))
- | A.Literal (`Keyword (s,x))
- | A.Literal (`Number (s,x)) ->
+ | A.Literal (_,`Symbol (s,x))
+ | A.Literal (_,`Keyword (s,x))
+ | A.Literal (_,`Number (s,x)) ->
let attr =
match x with
| None, None -> []
let env'' = Env.remove_name env' acc_name in
match aux acc with
| None -> aux_base term
- | Some (base_env, ctors', rec_envl) ->
- let ctors'' = ctors' @ ctors in
+ | Some (base_env, ctors_acc, rec_envl) ->
+ let ctors'' = ctors' @ ctors_acc (* @ ctors *)in
Some (base_env, ctors'',env'' :: rec_envl)
end
in
match aux term with
| None -> None
- | Some (base_env, ctors, rec_envl) ->
+ | Some (base_env, ctors_term, rec_envl) ->
let env' =
base_env @ Env.coalesce_env p_rec_decls rec_envl @ env
(* @ env LUCA!!! *)
in
- Some (env', ctors))
+ Some (env', ctors_term @ ctors))
| Ast.Default (p_some, p_none) -> (* p_none can't bound names *)
let p_some_decls = Env.declarations_of_term p_some in
let hvbox = box Ast.HV
let hovbox = box Ast.HOV
let break = Ast.Layout Ast.Break
-let space = Ast.Literal (`Symbol ("Â ", (None,None)))
-let builtin_symbol s = Ast.Literal (`Symbol (s,(None,None)))
-let keyword k = add_keyword_attrs (Ast.Literal (`Keyword (k,(None,None))))
+let space = Ast.Literal (None,`Symbol ("Â ", (None,None)))
+let builtin_symbol s = Ast.Literal (None,`Symbol (s,(None,None)))
+let keyword k = add_keyword_attrs (Ast.Literal (None,`Keyword (k,(None,None))))
let number s =
add_xml_attrs (* (RenderingAttrs.number_attributes `MathML) *) ()
- (Ast.Literal (`Number (s,(None,None))))
+ (Ast.Literal (None,`Number (s,(None,None))))
let ident i =
add_xml_attrs (* (RenderingAttrs.ident_attributes `MathML) *) ()
in
[ value ]
| Ast.Magic m -> subst_magic pos env m
- | Ast.Literal l as t ->
- (match idrefs with
- | [] -> [t]
- | desc::_ ->
+ | Ast.Literal (csym,l) as t ->
+ let enrich_literal l (_,uri,desc) =
let desc = Some desc in
- (match l with
- | `Keyword (k,_) -> [ Ast.Literal (`Keyword (k,(None,desc))) ]
- | `Symbol (s,_) -> [ Ast.Literal (`Symbol (s,(None,desc))) ]
- | `Number (n,_) -> [ Ast.Literal (`Number (n,(None,desc))) ]))
+ match l with
+ | `Keyword (k,_) -> [ Ast.Literal (csym,`Keyword (k,(uri,desc))) ]
+ | `Symbol (s,_) -> [ Ast.Literal (csym,`Symbol (s,(uri,desc))) ]
+ | `Number (n,_) -> [ Ast.Literal (csym,`Number (n,(uri,desc))) ]
+ in
+ (match csym,idrefs with
+ | None, [] -> [t]
+ | None,disamb::_ -> enrich_literal l disamb
+ | Some cs,_ ->
+ (try
+ let disamb = List.find (fun (cs',_,_) -> cs = cs') idrefs in
+ enrich_literal l disamb
+ with Not_found ->
+ (* prerr_endline ("can't find idref for " ^ cs ^ ". Will now print idrefs");
+ List.iter
+ (fun (cs'',_,_) -> prerr_endline ("idref " ^ cs''))
+ idrefs;*)
+ [t]))
| Ast.Layout l -> [ Ast.Layout (subst_layout pos env l) ]
| t -> [ NotationUtil.visit_ast (subst_singleton pos env) t ]
and subst_magic pos env = function
let sep =
match sep_opt with
| None -> []
- | Some l -> [ Ast.Literal l; break; space ]
+ | Some l -> [ Ast.Literal (None,l); break; space ]
in
let rec instantiate_list acc = function
| [] -> List.rev acc
let head_names names env =
let rec aux acc = function
- | (name, (ty, v)) :: tl when List.mem name names ->
+ | (name, (ty, v)) as x :: tl when List.mem name names ->
(match ty, v with
| Env.ListType ty, Env.ListValue (v :: _) ->
- aux ((name, (ty, v)) :: acc) tl
+ aux ((name, (ty,v)):: acc) tl
| Env.TermType _, Env.TermValue _ ->
- aux ((name, (ty, v)) :: acc) tl
+ aux (x :: acc) tl
| Env.OptType _, Env.OptValue _ ->
- aux ((name, (ty, v)) :: acc) tl
+ aux (x :: acc) tl
| _ -> assert false)
+ | (_,(_,Env.DisambiguationValue _)) as x :: tl ->
+ aux (x::acc) tl
| _ :: tl -> aux acc tl
(* base pattern may contain only meta names, thus we trash all others *)
| [] -> acc
in
aux [] env
-let instantiate_level2 status env (loc,uri,desc) term =
+let instantiate_level2 status env (* (loc,uri,desc) *) term =
(* prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
let fresh_env = ref [] in
let lookup_fresh_name n =
| Ast.Num _
| Ast.Sort _
| Ast.UserInput -> term
- | Ast.Symbol (s,_) -> aux_symbol s loc (uri,desc)
+ | Ast.Symbol (s,_) -> aux_symbol s (List.map (fun (_,(_,x)) -> x) env)
| Ast.Magic magic -> aux_magic env magic
| Ast.Variable var -> aux_variable env var
| Ast.Cast (t, ty) -> Ast.Cast (aux env t, aux env ty)
| _ -> assert false
- and aux_symbol s loc = function
- | _, None -> Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None))
- | uri, Some desc ->
- Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc)))
+ and aux_symbol s env =
+ (* XXX: it's totally unclear why the env we receive here is in reverse
+ * order (a diff with the previous revision shows no obvious reason).
+ * This one-line patch is needed so that the default symbol chosen for
+ * storing the interpretation is the leftmost, rather than the rightmost *)
+ let env = List.rev env in
+ try
+ (let dv =
+ try List.find (function
+ | Env.DisambiguationValue(Some s',_,_,_) when s = s' -> true
+ | _ -> false) env
+ with Not_found ->
+ List.find (function
+ | Env.DisambiguationValue(None,_,_,_) -> true
+ | _ -> false) env
+ in
+ match dv with
+ | Env.DisambiguationValue(_,loc,uri,Some desc) ->
+ Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, Some (uri,desc)))
+ | Env.DisambiguationValue(_,loc,_,_) ->
+ (* The important disambiguation info for symbols is the desc,
+ * if we don't have it, we won't use the uri either *)
+ Ast.AttributedTerm (`Loc loc, Ast.Symbol (s, None))
+ | _ -> assert false) (* vacuous *)
+ with Not_found ->
+ (* Ast.AttributedTerm (`Loc Stdpp.dummy_loc, Ast.Symbol (s, None))*)
+ Ast.Symbol (s, None)
and aux_opt env = function
| Some term -> Some (aux env term)
| None -> None
(** fills a term pattern instantiating variable magics *)
val instantiate_level2:
#NCic.status -> NotationEnv.t ->
- Stdpp.location * string option * string option ->
NotationPt.term -> NotationPt.term
do_heavy_checks: bool ;
}
-let prerr_endline _ = ()
+let prerr_endline _ = ()
let basic_eval_unification_hint (t,n) status =
NCicUnifHint.add_user_provided_hint status t n
let basic_eval_input_notation (l1,l2) status =
GrafiteParser.extend status l1
(fun env loc ->
- let rec get_disamb = function
+ (* let rec get_disamb = function
| [] -> Stdpp.dummy_loc,None,None
- | (_,(NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
+ | (_,(csym,NotationEnv.NoType,NotationEnv.DisambiguationValue dv))::_ -> dv
| _::tl -> get_disamb tl
- in
- let l2' = TermContentPres.instantiate_level2 status env (get_disamb env) l2 in
+ in *)
+ let l2' =
+ TermContentPres.instantiate_level2 status env (*(get_disamb env)*) l2 in
prerr_endline ("new l2 ast : " ^ (NotationPp.pp_term status l2'));
NotationPt.AttributedTerm (`Loc loc,l2'))
;;
{status#disambiguate_db with interpr = interpr }
in
status#set_disambiguate_db new_status
-
+
+(*
+let print_interpr status =
+ DisambiguateTypes.InterprEnv.iter
+ (fun loc alias ->
+ let start,stop = HExtlib.loc_of_floc loc in
+ let strpos = Printf.sprintf "@(%d,%d):" start stop in
+ match alias with
+ | GrafiteAst.Ident_alias (id,uri) ->
+ Printf.printf "%s [%s;%s]\n" strpos id uri
+ | GrafiteAst.Symbol_alias (name,_ouri,desc) ->
+ Printf.printf "%s <%s:%s>\n" strpos name desc
+ | GrafiteAst.Number_alias (_ouri,desc) ->
+ Printf.printf "%s <NUM:%s>\n" strpos desc)
+ status#disambiguate_db.interpr
+*)
+
let add_to_disambiguation_univ status new_aliases =
let multi_aliases =
List.fold_left (fun acc (d,c) ->
#status as 'status ->
(Stdpp.location * GrafiteAst.alias_spec) list -> 'status
+(* val print_interpr:
+ #status as 'status -> unit *)
+
val add_to_disambiguation_univ:
#status as 'status ->
(DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status
let rec get_ast status ~compiling ~asserted ~include_paths strm =
match GrafiteParser.parse_statement status strm with
(GrafiteAst.Executable
- (_,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
+ (loc,GrafiteAst.NCommand (_,GrafiteAst.Include (_,_,mafilename)))) as cmd
->
let already_included = NCicLibrary.get_transitively_included status in
let asserted,_ =
match cont with
| 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, str
with exn when not matita_debug ->
- prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn);
+ (* prerr_endline ("EnrichedWithStatus: " ^ Printexc.to_string exn); *)
raise (EnrichedWithStatus (exn, status))
in
if stop then asserted,status else loop asserted status str
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;
- prerr_endline ("now generating disambiguated script for " ^ fname);
let origbuf = Ulexing.from_utf8_channel (open_in fname) in
let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in
let outstr = ref "" in
ignore (SmallLexer.mk_small_printer interpr outstr origbuf);
Printf.fprintf outch "%s" !outstr;
- prerr_endline ("returning after compilation of " ^ fname);
asserted
(* MATITA 1.0: debbo fare time_travel sulla ng_library?
LexiconSync.time_travel
let ngtime_of baseuri =
let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in
let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in
- prerr_endline ("uid = " ^ uid);
- prerr_endline ("ngpath = " ^ ngpath);
+ (* prerr_endline ("uid = " ^ uid);
+ prerr_endline ("ngpath = " ^ ngpath); *)
try
Some (Unix.stat ngpath).Unix.st_mtime
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
asserted, children_bad || matime > ngtime
| None -> asserted,true
in
- prerr_endline ("asserted = " ^ (String.concat "," asserted));
+ (* prerr_endline ("asserted = " ^ (String.concat "," asserted)); *)
if not to_be_compiled then fullmapath::asserted,false
else
if List.mem baseuri already_included then
| None -> open_out (fullmapath ^ ".mad"), true
| Some c -> c, false
in
- prerr_endline ("compiling " ^ fullmapath);
+ (* prerr_endline ("compiling " ^ fullmapath); *)
let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in
if is_file_ch then close_out outch;
fullmapath::asserted,true
module Stack = Continuationals.Stack
+let debug = prerr_endline
(* disable for debug *)
let prerr_endline _ = ()
Http_daemon.respond ~headers:["Content-Type", contenttype] ~code:(`Code 200) ~body:s outchan
;;
-let retrieve (cgi : Netcgi.cgi_activation) =
+let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(try
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
in raise (Disamb_error strchoices)
| GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l))
(* | End_of_file -> ... *)
- | e -> raise e
+ | e ->
+ prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e);
+ raise e
in
try
eval_statement !include_paths (*buffer*) status (`Raw text)
with e -> do_exc e
in
+ debug "BEGIN PRINTGRAMMAR";
+ (*prerr_endline (Print_grammar.ebnf_of_term status);*)
+ (*let kwds = String.concat ", " status#get_kwds in
+ debug ("keywords = " ^ kwds );*)
+ debug "END PRINTGRAMMAR";
MatitaAuthentication.set_status sid st;
MatitaAuthentication.set_history sid (st::history);
(* prerr_endline "previous timestamp";
Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
() (html_of_matita new_statements), new_unparsed, st
-let register (cgi : Netcgi.cgi_activation) =
+let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let _env = cgi#environment in
assert (cgi#arguments <> []);
cgi#out_channel#commit_work()
;;
-let login (cgi : Netcgi.cgi_activation) =
+let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
assert (cgi#arguments <> []);
cgi#out_channel#commit_work()
;;
-let logout (cgi : Netcgi.cgi_activation) =
+let logout (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(try
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
exception File_already_exists;;
-let save (cgi : Netcgi.cgi_activation) =
+let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(try
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
cgi#out_channel#commit_work()
;;
-let initiate_commit (cgi : Netcgi.cgi_activation) =
+let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(try
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
cgi#out_channel#commit_work()
;;
-let svn_update (cgi : Netcgi.cgi_activation) =
+let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
let sid = HExtlib.unopt sid in
(* returns the length of the executed text and an html representation of the
* current metasenv*)
(*let advance =*)
-let advance (cgi : Netcgi.cgi_activation) =
- (* let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in *)
+let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(try
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
cgi#out_channel#commit_work()
;;
-let gotoBottom (cgi : Netcgi.cgi_activation) =
+let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(* (try *)
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
cgi#out_channel#commit_work()
;;
-let gotoTop (cgi : Netcgi.cgi_activation) =
+let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
prerr_endline "executing goto Top";
(try
cgi#out_channel#commit_work()
;;
-let retract (cgi : Netcgi.cgi_activation) =
+let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
(try
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
;;
-let viewLib (cgi : Netcgi.cgi_activation) =
+let viewLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
let env = cgi#environment in
let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
;;
-let resetLib (cgi : Netcgi.cgi_activation) =
+let resetLib (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
MatitaAuthentication.reset ();
cgi # set_header
~cache:`No_cache
matita.disambMode = true;
updateSide();
- throw "Stop";
+ throw "Wait";
}
else if (is_defined(disamberr)) {
// must be fixed in a daemon: it makes sense to return a
matita.disambMode = true;
next_cp(0);
}
- throw "Stop";
+ throw "Wait";
}
else {
var error = xml.getElementsByTagName("error")[0];
debug("advance failed");
}
} catch (e) {
- // nothing to do
+ if (e == "Stop")
+ resume();
+ else
+ pause();
};
- resume();
};
pause();
callServer("advance",processor,"body=" + (unlocked.innerHTML.html_to_matita()).sescape());
var tryagainbutton = document.createElement("input");
tryagainbutton.setAttribute("type","button");
if (new_curcp > 0) {
- tryagainbutton.setAttribute("value","Try something else");
+ tryagainbutton.setAttribute("value","None of the above");
} else {
tryagainbutton.setAttribute("value","Restart");
}
cancelbutton.setAttribute("onclick","cancel_disambiguate()");
var backbutton = document.createElement("input");
backbutton.setAttribute("type","button");
- backbutton.setAttribute("value","<< Back");
+ backbutton.setAttribute("value","<< Go back");
backbutton.setAttribute("onclick","next_cp(" + cpno + ")");
disambcell.appendChild(backbutton);
} catch (er) {
init_autotraces();
populate_goalarray(metasenv);
- resume();
+ if (er == "Stop")
+ resume();
+ else
+ pause();
+
}
} else {
init_autotraces();
projects / helm.git / commitdiff