1 files changed, 126 insertions, 0 deletions
diff --git a/isabelle-proto/src/session.rs b/isabelle-proto/src/session.rs
new file mode 100644
index 0000000..85081d4
--- /dev/null
+++ b/isabelle-proto/src/session.rs
@@ -0,0 +1,126 @@
+use std::{io::{BufRead, BufReader, Write}, process::{ChildStdin, ChildStdout, Command, Stdio}};
+
+use regex::Regex;
+use serde::de::DeserializeOwned;
+use serde_json::Value;
+
+use crate::{AsyncAnswer, ClientCommand, Encode, SessionStartedFinished, UseTheoriesFinished, decode_async, get_async_task_id, wait_for_client};
+
+
+
+
+pub struct IsabelleSession {
+    reader : BufReader<ChildStdout>,
+    writer : ChildStdin,
+    session_id : Option<String>
+}
+
+impl IsabelleSession {
+    pub fn start_with_client() -> Self {
+        let mut child = Command::new("isabelle")
+            .arg("client")
+            .stdin(Stdio::piped())
+            .stdout(Stdio::piped())
+            .stderr(Stdio::piped())
+            .spawn()
+            .expect("failed to run isabelle client!");
+
+        let mut reader = BufReader::new(child.stdout.take().unwrap());
+        let a = wait_for_client(&mut reader);
+        println!("client hello: {:?}", a);
+        IsabelleSession {
+            writer: child.stdin.unwrap(),
+            reader,
+            session_id: None
+        }
+    }
+
+    pub  fn start_session(&mut self, session : String, include_sessions : Vec<String>)
+        -> Result<SessionStartedFinished, Value>
+    {
+
+        self.writer.write(ClientCommand::SessionStart {
+            session, include_sessions
+        }.encode().as_bytes()).unwrap();
+        let task_id = get_async_task_id(&mut self.reader);
+        let started = self.await_task::<SessionStartedFinished, Value, Value,_>(&task_id, |_n| {})
+        //    .await
+            .unwrap();
+
+        match started {
+            Ok(ref finished) => self.session_id = Some(finished.session_id.to_owned()),
+            Err(_) => ()
+        };
+
+        started
+    }
+
+
+    pub fn load_theory(&mut self, theory : String, master_dir : Option<String>)
+    -> Result<UseTheoriesFinished, Value> {
+        let session_id = self.session_id.as_ref().unwrap();
+
+        self.writer.write(ClientCommand::UseTheories {
+            session_id: session_id.clone(),
+            theories: vec![ theory ],
+            master_dir,
+        }.encode().as_bytes()).unwrap();
+
+        let task_id = get_async_task_id(&mut self.reader);
+
+        self.await_task::<UseTheoriesFinished, Value, Value, _>(&task_id, |_| {})
+            .unwrap()
+    }
+
+
+
+    fn await_task<'a,T,E,N,F>(
+        &mut self,
+        task_id: &str,
+        mut prog: F)
+    -> Option<Result<T, E>>
+    where T: DeserializeOwned,
+          E: DeserializeOwned,
+          N: DeserializeOwned,
+          F: FnMut(N)
+    {
+        let reader = &mut self.reader;
+        for res in reader.lines() {
+            match res {
+                Err(err) => {
+                    eprintln!("error while reading from pipe: {}", err);
+                    std::process::exit(1);
+                },
+                Ok(line) => {
+                    let regex = Regex::new(r"^[0-9]+$").unwrap();
+                    if regex.is_match(&line) {
+                        // TODO: we don't support the long style of messages yet …
+                        // the following just assumes that the next blob is json
+                        // and does not contain line breaks.
+                    } else {
+                        // TODO: this shouldn't have to parse the json twice
+                        let value : Value = match decode_async(&line).unwrap() {
+                            AsyncAnswer::Finished(v) => v,
+                            AsyncAnswer::Failed(v) => v,
+                            AsyncAnswer::Note(v) => v
+                        };
+                        match value.get("task") {
+                            Some(id) if id == task_id =>
+                                Some(match decode_async::<T,E,N>(&line).unwrap() {
+                                    AsyncAnswer::Finished(data)
+                                        => return Some(Ok(data)),
+                                    AsyncAnswer::Failed(failed)
+                                        => return Some(Err(failed)),
+                                    AsyncAnswer::Note(val) => prog(val)
+
+                                }),
+                            _ => return None
+                        };
+                    }
+                }
+            }
+        }
+         unreachable!{}
+        None
+    }
+}