[ pages code ] Draft Predicate Logic introduction

Author: bobatkey

assets/local.css

@@ -5,6 +5,17 @@
     }
 }
 
+/* Monospace is easier to read when entering lots of symbols */
+
+input {
+    font-family: monospace;
+}
+
+/* Displayed formulas are centred. */
+
+.displayedformula {
+    text-align: center;
+}
 
 /* Code entry stuff */
 
@@ -24,6 +35,9 @@
     overflow:hidden;
     resize:none;
 }
+.defnsat-entry input {
+    width: 100%
+}
 
 .defnsat-parseresult {
     grid-column: 1;
@@ -74,10 +88,6 @@
 
 /* Natural deduction stuff */
 
-/* input { */
-/*     font-family: "DejaVu Sans Mono", "Linux Libertine O", "serif"; */
-/* } */
-
 .vertical {
     display:flex;
     flex-direction: column;
@@ -146,10 +156,9 @@
 }
 
 .comment {
-    color: #164; /* FIXME: dark mode? */
+    color: #164;
     font-style: italic;
     white-space: nowrap;
-    /* padding-left: 0.8em; */
 }
 
 @media (prefers-color-scheme: dark) {
@@ -191,10 +200,11 @@
 
 .resetbutton {
     padding: 0;
-    border: solid #ddd 1px;
-    font-size: 50%;
-    border-radius: 3px;
+    /*border: solid #ddd 1px;*/
+    font-size: 60%;
+    border-radius: 2px;
     margin-right: 0.3em;
+    opacity: 0.7;
 }
 
 /* ------------------------ */
@@ -235,19 +245,19 @@
 }
 
 .assumptionbox {
-  border-radius: 0.4em 0.4em 0 0;
-  border-top: 1px solid #ddd;
-  border-left: 1px solid #ddd;
-  border-right: 1px solid #ddd;
-  display: flex;
-  flex-direction: column;
-  margin-left: 0.5em; margin-right: 0.5em
+    border-radius: 0.4em 0.4em 0 0;
+    border-top: 1px solid #ddd;
+    border-left: 1px solid #ddd;
+    border-right: 1px solid #ddd;
+    display: flex;
+    flex-direction: column;
+    margin-left: 0.5em; margin-right: 0.5em
 }
 
 .assumption {
-  border-bottom: 1px solid #ddd;
-  margin-bottom: 1.2em;
-  color: #555;
-  font-style: italic;
-  padding-left: 0.5em
+    border-bottom: 1px solid #ddd;
+    margin-bottom: 1.2em;
+    color: #555;
+    font-style: italic;
+    padding-left: 0.5em
 }

frontend/frontend.ml

@@ -1,10 +1,28 @@
 open Widgets
 
+module Formula_validator = struct
+  open Fol_formula
+
+  type config = unit
+
+  let read_config _ = Some ()
+  let placeholder _ = "<formula>"
+  let validate _ str =
+    match Formula.of_string str with
+    | Ok f ->
+       Ok ("Formula is: " ^ Formula.to_string f)
+    | Error (`Parse err) ->
+       Error (Parser_util.Driver.string_of_error err)
+end
+
 let () =
   Ulmus.attach_all "lmt" Slakemoth_widget.component;
   Ulmus.attach_all "tickbox" Tickbox.component;
   Ulmus.attach_all "textbox" Textbox.component;
-  Ulmus.attach_all "entrybox" (Validating_entry.component (module Validating_entry.Null_Validator));
+  Ulmus.attach_all "entrybox"
+    (Validating_entry.component (module Validating_entry.Null_Validator));
+  Ulmus.attach_all "formulaentry"
+    (Validating_entry.component (module Formula_validator));
 
   Ulmus.attach_all "rules" Natural_deduction.Rules.from_rules;
   Ulmus.attach_all "rules-display" Natural_deduction.Rules.display_rules;

html_static/html_static.ml

@@ -229,6 +229,9 @@ let figcaption ?attrs = normal_element "figcaption" ?attrs
 let div ?attrs = normal_element "div" ?attrs
 let main ?attrs = normal_element "main" ?attrs
 
+let details ?attrs = normal_element "details" ?attrs
+let summary ?attrs = normal_element "summary" ?attrs
+
 (* 4.5 Text level semantics *)
 let a ?attrs = normal_element "a" ?attrs
 let em ?attrs = normal_element "em" ?attrs

html_static/html_static.mli

@@ -3,6 +3,9 @@
 include Html_sig.S
 (** Supports the generic HTML generation interface. *)
 
+val details : _ normal_element
+val summary : _ normal_element
+
 val raw_text : string -> _ t
 (** [raw_text str] produces a document consisting of [str] without
     escaping any of the HTML-sensitive characters. FIXME: better