Commit 3c88c175 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

ITP web: editor for source code made visible again in tab

parent 67930b18
......@@ -138,17 +138,13 @@ body {
}
/*** MAIN EDITOR ***/
#why3-editor-container {
position:relative;
flex-grow:2;
}
#why3-tab-container {
flex-grow:1;
position:relative;
margin:0;
padding:0;
}
#why3-editor {
position:absolute;
top:0;
......@@ -158,19 +154,6 @@ body {
padding:0;
margin:0;
}
#why3-editor-bg {
display:none;
position:absolute;
opacity:0.75;
top:0;
left:0;
width:100%;
height:100%;
z-index:100;
}
#why3-editor-bg:hover {
cursor:progress;
}
/*** TABS ***/
......@@ -229,6 +212,11 @@ body {
width:100%;
height:100%;
}
#why3-editor {
overflow:auto;
width:100%;
height:100%;
}
#why3-error-container {
overflow:auto;
width:100%;
......
......@@ -100,8 +100,7 @@
<span class="why3-tab-label why3-widget why3-inactive">Source code</span>
<div class="why3-widget why3-tab">
<div id="why3-editor-container" class="why3-container">
<div id="why3-editor-bg" class="why3-widget"> </div>
<div id="why3-editor" tabindex="-1" ></div>
<div id="why3-editor">Ceci est le code source</div>
</div>
</div>
<span class="why3-tab-label why3-widget why3-inactive">Log</span>
......
......@@ -181,7 +181,7 @@ module Editor =
let get_value ?(editor=editor) () : Js.js_string Js.t =
JSU.meth_call editor "getValue" [| |]
let set_value ?(editor=editor) (str : Js.js_string Js.t) =
let set_value ~editor (str : Js.js_string Js.t) =
ignore JSU.(meth_call editor "setValue" [| inject (str); inject ~-1 |])
let _Range = Js.Unsafe.global##._Range
......@@ -232,7 +232,7 @@ module Editor =
ignore JSU.(meth_call editor "on" [| inject (Js.string e);
inject f|])
(*
let editor_bg = getElement AsHtml.div "why3-editor-bg"
let disable () =
......@@ -243,7 +243,7 @@ module Editor =
let enable () =
ignore JSU.(meth_call editor "setReadOnly" [| inject Js._false|]);
editor_bg ##. style ##. display := Js.string "none"
*)
let confirm_unsaved () =
if not !saved then
......@@ -278,12 +278,14 @@ module ContextMenu =
if !enabled then
task_menu ##. style ##. display := Js.string "none"
(*
let add_action b f =
b ##. onclick := Dom.handler (fun _ ->
hide ();
f ();
Editor.(focus editor);
Js._false)
*)
let () = addMouseEventListener false task_menu "mouseleave"
(fun _ -> hide())
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment