mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-16 00:09:31 -06:00
904e8029fe
- separate tree edit buttons from option buttons - fix bug when wrapping on freshly imported ast - add interface for import & export of ast - cleaner internal implementation of Editor.add_refinement - small style updates
120 lines
1.6 KiB
CSS
120 lines
1.6 KiB
CSS
body.syntax-editor {
|
|
background: #ccc url("../minibar/brushed-metal.png");
|
|
}
|
|
|
|
.hidden
|
|
{
|
|
display:none;
|
|
}
|
|
|
|
.editor select#to_menu
|
|
{
|
|
height: 10em;
|
|
position: absolute;
|
|
min-width: 5em;
|
|
}
|
|
|
|
#import
|
|
{
|
|
position: absolute;
|
|
display: inline-block;
|
|
padding: 0.3em;
|
|
background: #EEE;
|
|
border: 1px solid #999;
|
|
font-size: 0.95em;
|
|
box-shadow: 2px 2px 4px rgba(0, 0, 0, 0.3);
|
|
}
|
|
#import.hidden
|
|
{
|
|
display: none;
|
|
}
|
|
#import input[type=text]
|
|
{
|
|
width: 20em;
|
|
font-family: monospace;
|
|
padding: 0.2em;
|
|
}
|
|
|
|
#tree
|
|
{
|
|
white-space:pre;
|
|
font-family: monospace;
|
|
background: rgba(238, 238, 238, 0.6);
|
|
padding:0.5em;
|
|
margin:0.5em 0;
|
|
}
|
|
|
|
#tree .node
|
|
{
|
|
margin: 0.4em 0 0.4em 1.5em;
|
|
}
|
|
|
|
#tree .node a
|
|
{
|
|
cursor: pointer;
|
|
}
|
|
#tree .node a:hover
|
|
{
|
|
text-decoration: underline;
|
|
}
|
|
#tree .node a.current
|
|
{
|
|
font-weight: bold;
|
|
}
|
|
|
|
#refinements
|
|
{
|
|
/* display: inline-block; */
|
|
/* margin-left: 0.5em; */
|
|
margin-top: 0.3em;
|
|
}
|
|
|
|
#linearisations
|
|
{
|
|
/* background: rgba(170, 170, 170, 0.5); */
|
|
padding:0.5em;
|
|
margin:0.5em 0;
|
|
}
|
|
#linearisations div
|
|
{
|
|
padding:0.2em;
|
|
}
|
|
#linearisations .lang
|
|
{
|
|
display: inline-block;
|
|
margin-right: 0.5em;
|
|
width: 3em;
|
|
font-weight: bold;
|
|
text-align: center;
|
|
}
|
|
#linearisations .lin
|
|
{
|
|
}
|
|
|
|
.refinement
|
|
{
|
|
margin: 0.1em;
|
|
display: inline-block;
|
|
cursor: pointer;
|
|
border: 1px solid;
|
|
padding: 0.2em;
|
|
font: 0.9em sans-serif;
|
|
background: white;
|
|
box-shadow: 2px 2px 4px rgba(0, 0, 0, 0.3);
|
|
}
|
|
.refinement.disabled
|
|
{
|
|
opacity: 0.5;
|
|
}
|
|
|
|
#debug
|
|
{
|
|
font: 10px monospace;
|
|
white-space: pre;
|
|
color: #333;
|
|
margin: 1em 0;
|
|
border: 1px dashed #999;
|
|
padding: 1em;
|
|
}
|
|
|