module Ast = NotationPt
-(* the integer is an offset to be added to each location *)
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
exception NoWellTypedInterpretation of
int *
((Stdpp.location list * string * string) list *
type domain = domain_tree list
and domain_tree = Node of Stdpp.location list * domain_item * domain
+(*
let mono_uris_callback ~selection_mode ?ok
?(enable_button_for_non_vars = true) ~title ~msg ~id =
if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
else
raise Ambiguous_input
-let mono_interp_callback _ _ _ = raise Ambiguous_input
-let mono_disamb_callback _ = raise Ambiguous_input
+let mono_interp_callback _ _ _ = assert false
+let mono_disamb_callback _ = assert false
let _choose_uris_callback = ref mono_uris_callback
let _choose_interp_callback = ref mono_interp_callback
let interactive_user_uri_choice = !_choose_uris_callback
let interactive_interpretation_choice interp = !_choose_interp_callback interp
let interactive_ast_choice interp = !_choose_disamb_callback interp
+*)
+
let input_or_locate_uri ~(title:string) ?id () = None
(* Zack: I try to avoid using this callback. I therefore assume that
* the presence of an identifier that can't be resolved via "locate"
in
match res with
| [] -> raise (NoWellTypedInterpretation (0,[]))
+ (* XXX : the boolean seems not to play a role any longer *)
| [t] -> res,false
- | _ ->
- let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in
+ | _ -> res, true
+ (* let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in
let user_choice = interactive_ast_choice choices in
[ List.nth res user_choice ], true
(* let pp_thing (t,_,_,_,_,_) = prerr_endline ("interpretation: " ^ (pp_thing t)) in
- List.iter pp_thing res; res,true *)
+ List.iter pp_thing res; res,true *) *)
;;
(** {2 Disambiguation interface} *)
-(** raised when ambiguous input is found but not expected (e.g. in the batch
- * compiler) *)
-exception Ambiguous_input
-
(* the integer is an offset to be added to each location *)
(* list of located error messages, each list is a tuple:
* - environment in string form
exception Try_again of string Lazy.t
+(*
val set_choose_uris_callback:
DisambiguateTypes.interactive_user_uri_choice_type -> unit
* choose_interp_callback if not set otherwise with set_choose_interp_callback
* above *)
val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
+*)
val resolve :
env:'alias1 DisambiguateTypes.InterprEnv.t ->
new_aliases,res
;;*)
+(* reports the first source of ambiguity and its possible interpretations *)
+exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list)
+
let dump_aliases out msg status =
out (if msg = "" then "aliases dump:" else msg ^ ": aliases dump:");
DisambiguateTypes.InterprEnv.iter (fun _ x -> out (GrafiteAstPp.pp_alias x))
exception BaseUriNotSetYet
-let singleton msg = function
- | [x], _ -> x
- | l, _ ->
- let debug =
- Printf.sprintf "GrafiteDisambiguate.singleton (%s): %u interpretations"
- msg (List.length l)
- in
- prerr_endline debug; assert false
-
let __Implicit = "__Implicit__"
let __Closed_Implicit = "__Closed_Implicit__"
| _ -> assert false
;;
+(* this function, called on a list of choices that must
+ * be different, never fails and returns the location of
+ * the first ambiguity (and its possible interpretations) *)
+let rec find_diffs l =
+ let loc,_ = List.hd (List.hd l) in
+ let hds = List.map (fun x -> snd (List.hd x)) l in
+ let uniq_hds = HExtlib.list_uniq hds in
+
+ if List.length uniq_hds > 1
+ then loc, uniq_hds
+ else
+ let tls = List.map List.tl l in
+ find_diffs tls
+;;
+
let disambiguate_nterm status expty context metasenv subst thing
-=
- let newast, metasenv, subst, cic =
- singleton "first"
- (NCicDisambiguate.disambiguate_term
+=
+ let choices, _ = NCicDisambiguate.disambiguate_term
status
~aliases:status#disambiguate_db.interpr
~expty
~mk_choice:(ncic_mk_choice status)
~mk_implicit ~fix_instance
~description_of_alias:GrafiteAst.description_of_alias
- ~context ~metasenv ~subst thing)
+ ~context ~metasenv ~subst thing
in
let _,_,thing' = thing in
- let diff = diff_term Stdpp.dummy_loc thing' newast in
- let status = add_to_interpr status diff
- in
- metasenv, subst, status, cic
+ match choices with
+ | [newast, metasenv, subst, cic] ->
+ let diff = diff_term Stdpp.dummy_loc thing' newast in
+ let status = add_to_interpr status diff
+ in
+ metasenv, subst, status, cic
+ | [] -> assert false
+ | _ ->
+ let diffs =
+ List.map (fun (ast,_,_,_) ->
+ diff_term Stdpp.dummy_loc thing' ast) choices
+ in
+ raise (Ambiguous_input (find_diffs diffs))
;;
-
type pattern =
NotationPt.term Disambiguate.disambiguator_input option *
(string * NCic.term) list * NCic.term option
metasenv, `Auto params
;;
-let disambiguate_nobj status ?baseuri (text,prefix_len,obj) =
+let disambiguate_nobj status ?baseuri (text,prefix_len,obj as obj') =
let uri =
let baseuri =
match baseuri with Some x -> x | None -> raise BaseUriNotSetYet
in
NUri.uri_of_string (baseuri ^ "/" ^ name)
in
- let ast, _, _, cic =
- singleton "third"
- (NCicDisambiguate.disambiguate_obj
+
+ let choices, _ = NCicDisambiguate.disambiguate_obj
status
~lookup_in_library:(nlookup_in_library status)
~description_of_alias:GrafiteAst.description_of_alias
~mk_implicit ~fix_instance ~uri
~aliases:status#disambiguate_db.interpr
~universe:(status#disambiguate_db.multi_aliases)
- (text,prefix_len,obj)) in
- let diff = diff_obj Stdpp.dummy_loc obj ast in
- let status = add_to_interpr status diff
+ obj'
in
- status, cic
+ match choices with
+ | [ast, _, _, cic] ->
+ let diff = diff_obj Stdpp.dummy_loc obj ast in
+ let status = add_to_interpr status diff
+ in
+ status, cic
+ | [] -> assert false
+ | _ ->
+ let diffs =
+ List.map (fun (ast,_,_,_) ->
+ diff_obj Stdpp.dummy_loc obj ast) choices
+ in
+ raise (Ambiguous_input (find_diffs diffs))
;;
let disambiguate_cic_appl_pattern status args =
(* args: print function, message (may be empty), status *)
val dump_aliases: (string -> unit) -> string -> #status -> unit
+(* reports the first source of ambiguity and its possible interpretations *)
+exception Ambiguous_input of (Stdpp.location * GrafiteAst.alias_spec list)
+
exception BaseUriNotSetYet
val disambiguate_nterm :
<head>
<script type="text/javascript" src="utf8MacroTable.js"></script>
<script type="text/javascript" src="matitaweb.js"></script>
+<script type="text/javascript" src="layout.js"></script>
<link rel="stylesheet" type="text/css" href="matitaweb.css"/>
<link href="treeview/xmlTree.css" type="text/css" rel="stylesheet"/>
</head>
-<body onLoad="initialize();">
+<body onLoad="initialize();" onResize="resize();">
<textarea id="unescape" style="display:none;"></textarea>
-<div id="sandbox" style="visibility:hidden;"></div>
+<div id="sandbox" style="display:none;"></div>
-<div class="matitaapparea">
+<div class="matitaapparea" id="matitaapparea">
-<div class="titlebar">
+<div class="titlebar" id="titlebar">
<div class="mainTitle"><H2 id="matitaTitle">Matita - <<Filename>></H2></div>
<div class="mainRight" id="matitaLogout"><A id="hlogout" href="/logout.html">Log out</A></div>
</div>
-<div class="toparea">
+<div class="toparea" id="toparea">
<div class="navibar">
<A href="javascript:advanceForm1()"><IMG class="topimg" src="icons/advance.png"
id="advance" alt="Advance"
<pre><div contentEditable="false" id="locked" style="background-color:#bfbfff; display:inline;"></div><div contentEditable="true" id="unlocked" style="display:inline">(* script *)</div></pre></div>
<!-- the script (end) -->
</div>
-<div class="goalarea" id="goalcell">
+<div class="sidearea" id="sidearea">
+ <div class="framed" id="disambcell"></div>
+ <div class="framed" id="goalcell">
<div id="goals"></div>
- <div contentEditable="true" style="border-style:solid; height:95%; width:100%; overflow:auto;">
+ <div class="context">
<pre id="goalview"></pre>
</div>
+ </div>
</div>
</div>
<div class="dialog" id="dialogBox" style="display: none;">
<div class="diaTitle" id="dialogTitle"></div>
- <div class="diaClose" id="dialogClose"><H2><A id="butClose" href="javascript:abortDialog()">X</A></H2></div>
+ <div class="diaClose" id="dialogClose"><H2><A class="butClose" href="javascript:abortDialog('dialogBox')">X</A></H2></div>
<INPUT type="button" id="dialogNewdir" value="Create dir..." ONCLICK="createDir()" style="width:150px"><br/>
<div class="scroll" id="dialogContent"></div>
<INPUT class="diaFile" type="text" id="dialogFilename">
<div class="upload" id="uploadBox" style="display: none;">
<div class="dialogTitle" id="uploadTitle"></div>
- <div class="diaClose" id="uploadClose"><H2><A id="but1Close" href="javascript:abortUpload()">X</A></H2></div>
+ <div class="diaClose" id="uploadClose"><H2><A class="butClose" href="javascript:abortDialog('uploadBox')">X</A></H2></div>
<INPUT class="diaFile" type="file" id="uploadFilename">
<INPUT type="button" id="uploadSelect" value="OK" ONCLICK="uploadOK()" style="width:70px">
</div>
</body>
- </html>
+</html>
open Http_types;;
exception Emphasized_error of string
+exception Ambiguous of string
module Stack = Continuationals.Stack
let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
() (html_of_matita marked) in
raise (Emphasized_error marked)
- | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
- let strchoices =
- String.concat "\n" (List.map
- GrafiteAst.description_of_alias choices)
- in
- let x,y = HExtlib.loc_of_floc loc in
- prerr_endline (Printf.sprintf
- "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End."
+ | GrafiteDisambiguate.Ambiguous_input (loc,choices) ->
+ let x,y = HExtlib.loc_of_floc loc in
+ let choice_of_alias = function
+ | GrafiteAst.Ident_alias (_,uri) -> uri, None, uri
+ | GrafiteAst.Number_alias (None,desc)
+ | GrafiteAst.Symbol_alias (_,None,desc) -> "cic:/fakeuri.def(1)", Some desc, desc
+ | GrafiteAst.Number_alias (Some uri,desc)
+ | GrafiteAst.Symbol_alias (_,Some uri,desc) -> uri, Some desc, desc
+ in
+ let tag_of_choice (uri,title,desc) =
+ match title with
+ | None -> Printf.sprintf "<choice href=\"%s\">%s</choice>"
+ uri
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+ | Some t -> Printf.sprintf "<choice href=\"%s\" title=\"%s\">%s</choice>"
+ uri
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () t)
+ (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () desc)
+ in
+ let strchoices =
+ String.concat "\n"
+ (List.map (fun x -> tag_of_choice (choice_of_alias x)) choices)
+ in
+ prerr_endline (Printf.sprintf
+ "@@@ Ambiguous input at (%d,%d). Possible choices:\n\n%s\n\n@@@ End."
x y strchoices);
+ (*
let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in
let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in
let post = Netconversion.ustring_sub `Enc_utf8 y
pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in
let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false
() (html_of_matita marked) in
- raise (Emphasized_error marked)
+ *)
+ let strchoices = Printf.sprintf
+ "<ambiguity start=\"%d\" stop=\"%d\">%s</ambiguity>" x y strchoices
+ in raise (Ambiguous strchoices)
(* | End_of_file -> ... *)
in
let stringbuf = Ulexing.from_utf8_string new_statements in
with
| Emphasized_error text ->
(* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *)
- let body = "<response><error>" ^ text ^ "</error> </response>" in
+ let body = "<response><error>" ^ text ^ "</error></response>" in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string body
+ | Ambiguous text ->
+ let body = "<response>" ^ text ^ "</response>" in
cgi # set_header
~cache:`No_cache
~content_type:"text/xml; charset=\"utf-8\""
+body {
+ border:0px;
+ padding:0px;
+ margin:0px;
+}
+
+div#matitaapparea {
+ border:0px;
+ padding:0px;
+ margin:0px;
+ position:fixed;
+}
+
div.upload {
position:absolute;
top: 50%;
div.titlebar {
display: block;
- margin-left: auto;
- margin-right: auto;
- margin-bottom: 4px;
+ margin:0px;
+ border:0px;
width:100%;
height: 32px;
background-color: #007fff;
color: inherit;
font-weight: bold;
}
-a#butClose {
+
+a.butClose {
color: inherit;
}
div.toparea {
display: block;
+ padding:4px;
margin-left: auto;
margin-right: auto;
height:64px;
div.workarea {
display: block;
- margin-left: auto;
- margin-right: auto;
+ border:0px;
+ padding:0px;
+ margin:0px;
+ /*margin-left: auto;
+ margin-right: auto;*/
height:84%;
width:100%;
}
div.scriptarea {
display: inline-block;
- margin-left: auto;
- margin-right: auto;
+ border:0px;
+ padding:0px;
+ margin:0px;
+/* margin-left: auto;
+ margin-right: auto;*/
height:100%;
- width:67%%;
+ width:67%;
min-width:67%;
max-width:67%;
float:left;
}
-div.goalarea {
+div.sidearea {
display: inline-block;
- margin-left: auto;
- margin-right: auto;
+ border:0px;
+ padding:0px;
+ margin:0px;
+ /*margin-left: auto;
+ margin-right: auto;*/
height:100%;
width:33%;
min-width:33%;
float:right;
}
+div.framed {
+ border: 2px solid DarkGray;
+}
+
+div.context {
+ overflow: auto;
+}
+
span.activegoal {
color: red;
font-weight: bold;
var dialogContent;
var metasenv = "";
var lockedbackup = "";
+var matita;
function text_of_html(h)
{
if (readCookie("session") == null) {
window.location = "/login.html"
} else {
+ body = document.body;
+ titlebar = document.getElementById("titlebar");
matitaTitle = document.getElementById("matitaTitle");
+ apparea = document.getElementById("matitaapparea");
locked = document.getElementById("locked");
unlocked = document.getElementById("unlocked");
+ toparea = document.getElementById("toparea");
workarea = document.getElementById("workarea");
scriptcell = document.getElementById("scriptcell");
+ sidearea = document.getElementById("sidearea");
+ disambcell = document.getElementById("disambcell");
goalcell = document.getElementById("goalcell");
goals = document.getElementById("goals");
goalview = document.getElementById("goalview");
cursorButton = document.getElementById("cursor");
bottomButton = document.getElementById("bottom");
dialogBox = document.getElementById("dialogBox");
+ uploadBox = document.getElementById("uploadBox");
dialogTitle = document.getElementById("dialogTitle");
dialogContent = document.getElementById("dialogContent");
- changeFile("test.ma");
-
+ matita = new Object();
+ matita.disambMode = matita.proofMode = false;
+
// hide sequent view at start
- hideSequent();
+ initializeLayout();
+ updateSide();
+
+ changeFile("test.ma");
// initialize keyboard events in the unlocked script
init_keyboard(unlocked);
{
processor = function(xml) {
if (is_defined(xml)) {
- parsed = xml.getElementsByTagName("parsed")[0];
+ var parsed = xml.getElementsByTagName("parsed")[0];
+ var ambiguity = xml.getElementsByTagName("ambiguity")[0];
if (is_defined(parsed)) {
// debug("advance: received response\nBEGIN\n" + req.responseText + "\nEND");
- len = parseInt(parsed.getAttribute("length"));
+ var len = parseInt(parsed.getAttribute("length"));
// len0 = unlocked.innerHTML.length;
- unescaped = unlocked.innerHTML.html_to_matita();
- parsedtxt = parsed.childNodes[0].nodeValue;
+ var unescaped = unlocked.innerHTML.html_to_matita();
+ var parsedtxt = parsed.childNodes[0].nodeValue;
//parsedtxt = unescaped.substr(0,len);
- unparsedtxt = unescaped.substr(len);
+ var unparsedtxt = unescaped.substr(len);
lockedbackup += parsedtxt;
locked.innerHTML = lockedbackup;
unlocked.innerHTML = unparsedtxt.matita_to_html();
// len1 = unlocked.innerHTML.length;
// len2 = len0 - len1;
- len2 = parsedtxt.length;
- metasenv = xml.getElementsByTagName("meta");
+ var len2 = parsedtxt.length;
+ var metasenv = xml.getElementsByTagName("meta");
populate_goalarray(metasenv);
statements = listcons(len2,statements);
unlocked.scrollIntoView(true);
}
+ else if (is_defined(ambiguity)) {
+ var start = parseInt(ambiguity.getAttribute("start"));
+ var stop = parseInt(ambiguity.getAttribute("stop"));
+ var choices = xml.getElementsByTagName("choice");
+
+ matita.ambiguityStart = start;
+ matita.ambiguityStop = stop;
+ matita.unlockedbackup = unlocked.innerHTML;
+ matita.interpretations = [];
+
+ var unlockedtxt = unlocked.innerHTML;
+ var pre = unlockedtxt.substring(0,start);
+ var mid = unlockedtxt.substring(start,stop);
+ var post = unlockedtxt.substring(stop);
+ unlocked.innerHTML = pre +
+ "<span class=\"error\" title=\"disambiguation error\">" +
+ mid + "</span>" + post;
+
+ var title = "<H3>Ambiguous input</H3>";
+ disambcell.innerHTML = title;
+ for (i = 0;i < choices.length;i++) {
+ matita.interpretations[i] = new Object();
+
+ var href = choices[i].getAttribute("href");
+ var title = choices[i].getAttribute("title");
+ var desc = choices[i].childNodes[0].nodeValue;
+
+ matita.interpretations[i].href = href;
+ matita.interpretations[i].title = title;
+ matita.interpretations[i].desc = desc;
+
+ var choice = document.createElement("input");
+ choice.setAttribute("type","radio");
+ choice.setAttribute("name","interpr");
+ choice.setAttribute("href",href);
+ choice.setAttribute("title",title);
+ if (i == 0) choice.setAttribute("checked","");
+
+ disambcell.appendChild(choice);
+ disambcell.appendChild(document.createTextNode(desc));
+ disambcell.appendChild(document.createElement("br"));
+ }
+
+ var okbutton = document.createElement("input");
+ okbutton.setAttribute("type","button");
+ okbutton.setAttribute("value","OK");
+ okbutton.setAttribute("onclick","do_disambiguate()");
+ var cancelbutton = document.createElement("input");
+ cancelbutton.setAttribute("type","button");
+ cancelbutton.setAttribute("value","Cancel");
+ cancelbutton.setAttribute("onclick","void(0)");
+
+ disambcell.appendChild(okbutton);
+ disambcell.appendChild(cancelbutton);
+
+ matita.disambMode = true;
+ updateSide();
+ }
else {
- error = xml.getElementsByTagName("error")[0];
+ var error = xml.getElementsByTagName("error")[0];
unlocked.innerHTML = error.childNodes[0].nodeValue;
// debug(xml.childNodes[0].nodeValue);
}
var goalcell;
function hideSequent() {
- goalcell.style.display = "none";
- scriptcell.style.width = "100%";
- scriptcell.style.minWidth = "100%";
- scriptcell.style.maxWidth = "100%";
+ matita.proofMode = false;
+ updateSide();
}
function showSequent() {
- scriptcell.style.width = "67%";
- scriptcell.style.minWidth = "67%";
- scriptcell.style.maxWidth = "67%";
- goalcell.style.display = "inline-block";
+ matita.proofMode = true;
+ updateSide();
}
function showDialog(title,content,callback) {
dialogBox.style.display = "block";
}
-function abortDialog() {
- dialogBox.style.display = "none";
+function showDisamb(content) {
+ disambContent.innerHTML = content;
+ disambBox.style.display = "block";
}
-function abortUpload() {
- uploadBox.style.display = "none";
+function abortDialog(dialog) {
+ dialogBox.style.display = "none";
}
function removeElement(id) {
debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
}
+function get_checked_index(name) {
+ var radios = document.getElementsByName(name);
+ for (i = 0; i < radios.length; i++) {
+ if (radios[i].checked) {
+ return i;
+ }
+ }
+ return null;
+}
+
+function do_disambiguate() {
+ var i = get_checked_index("interpr");
+ if (i != null) {
+ var pre = matita.unlockedbackup.substring(0,matita.ambiguityStart);
+ var mid = matita.unlockedbackup.substring(matita.ambiguityStart,matita.ambiguityStop);
+ var post = matita.unlockedbackup.substring(matita.ambiguityStop);
+
+ var href = matita.interpretations[i].href;
+ var title = matita.interpretations[i].title;
+
+ if (is_defined(title)) {
+ mid = "<A href=\"" + href + "\" title=\"" + title + "\">" + mid + "</A>";
+ } else {
+ mid = "<A href=\"" + href + "\">" + mid + "</A>";
+ }
+
+ unlocked.innerHTML = pre + mid + post;
+
+ matita.disambMode = false;
+ updateSide();
+ }
+}
+
function readCookie(name) {
var nameEQ = name + "=";
var ca = document.cookie.split(';');
projects / helm.git / commitdiff