From 6c84daf943dfba98f3061cba6adadc8837bf150a Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 27 Oct 2011 11:32:11 +0000 Subject: [PATCH] Matitaweb: Fixed a bug in matitaweb.js concerning disambiguation and escaping. Added pretty-printing of unhandled NTacStatus.Error exceptions. --- matitaB/matita/matitadaemon.ml | 8 ++++++++ matitaB/matita/matitaweb.js | 27 ++++++++++++++++++--------- 2 files changed, 26 insertions(+), 9 deletions(-) diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 9fc2b1bbc..a53d24f67 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -363,6 +363,14 @@ let advance0 sid text = let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita marked) in raise (Emphasized_error marked) + | NTacStatus.Error (s,None) as e -> + prerr_endline + ("NTacStatus.Error " ^ (Lazy.force s)); + raise e + | NTacStatus.Error (s,Some exc) as e -> + prerr_endline + ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc)); + raise e | GrafiteDisambiguate.Ambiguous_input (loc,choices) -> let x,y = HExtlib.loc_of_floc loc in let choice_of_alias = function diff --git a/matitaB/matita/matitaweb.js b/matitaB/matita/matitaweb.js index 890b34ec0..44fd608a1 100644 --- a/matitaB/matita/matitaweb.js +++ b/matitaB/matita/matitaweb.js @@ -575,13 +575,13 @@ function advanceForm1() matita.ambiguityStart = start; matita.ambiguityStop = stop; - matita.unlockedbackup = unlocked.innerHTML; + matita.unlockedbackup = unlocked.innerHTML.html_to_matita(); matita.interpretations = []; - var unlockedtxt = unlocked.innerHTML; - var pre = unlockedtxt.substring(0,start); - var mid = unlockedtxt.substring(start,stop); - var post = unlockedtxt.substring(stop); + var unlockedtxt = unlocked.innerHTML.html_to_matita(); + var pre = unlockedtxt.substring(0,start).matita_to_html(); + var mid = unlockedtxt.substring(start,stop).matita_to_html(); + var post = unlockedtxt.substring(stop).matita_to_html(); unlocked.innerHTML = pre + "" + mid + "" + post; @@ -618,7 +618,7 @@ function advanceForm1() var cancelbutton = document.createElement("input"); cancelbutton.setAttribute("type","button"); cancelbutton.setAttribute("value","Cancel"); - cancelbutton.setAttribute("onclick","void(0)"); + cancelbutton.setAttribute("onclick","cancel_disambiguate()"); disambcell.appendChild(okbutton); disambcell.appendChild(cancelbutton); @@ -1106,12 +1106,21 @@ function get_checked_index(name) { return null; } +function cancel_disambiguate() { + matita.disambMode = false; + updateSide(); +} + 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 pre = matita.unlockedbackup + .substring(0,matita.ambiguityStart).matita_to_html(); + var mid = matita.unlockedbackup + .substring(matita.ambiguityStart,matita.ambiguityStop) + .matita_to_html(); + var post = matita.unlockedbackup + .substring(matita.ambiguityStop).matita_to_html(); var href = matita.interpretations[i].href; var title = matita.interpretations[i].title; -- 2.39.2