actually usable code structure for isabelle-protoHEADmaster

3 files changed, 67 insertions, 95 deletions

diff --git a/isabelle-proto/src/main.rs b/isabelle-proto/src/main.rs
index 535dd52..1b52e27 100644
--- a/isabelle-proto/src/main.rs
+++ b/isabelle-proto/src/main.rs
@@ -1,104 +1,17 @@
 
 mod session;
 mod messages;
+mod pipe;
+
 
-use regex::Regex;
-use serde::{Deserialize, Serialize, de::DeserializeOwned};
-use serde_json::{Result, Value};
 use session::IsabelleSession;
-use messages::*;
 
 
-use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}};
-use std::fmt::Debug;
 
 
 use structopt::StructOpt;
 
 
-fn decode_sync<'a, T> (msg: &'a str) -> Option<SyncAnswer<T, String>>
-where T: Deserialize<'a> {
-    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
-    let mat = regex.find(msg)?;
-    let ty = &msg[..mat.end()];
-    let rest = &msg[mat.end()..];
-
-    match ty {
-        "OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)),
-        "ERROR" => Some(SyncAnswer::Error(rest.to_owned())),
-        _ => None
-    }
-}
-
-fn decode_async<'a,T,E,N> (msg: &'a str) -> Option<AsyncAnswer<T,E,N>>
-where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> {
-    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
-    let mat = regex.find(msg)?;
-    let ty = &msg[..mat.end()];
-    let rest = &msg[mat.end()..];
-
-    match ty {
-        "NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)),
-        "FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)),
-        "FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)),
-        _ => None
-    }
-}
-
-
-
-
-fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
-    for res in pipe.lines() {
-        match res {
-            Err(_) => (),
-            Ok(line) => {
-                let hello : Option<SyncAnswer<ClientHello, _>> = decode_sync(&line);
-                if let Some(SyncAnswer::Ok(data)) = hello {
-                    return Some(data);
-                }
-            }
-        }
-    }
-    None
-}
-
-
-fn wait_for_async_task<'a,T,E,N,F>
-    (reader: &mut BufReader<ChildStdout>, task: &str, mut prog: F) -> Option<T>
-where T: DeserializeOwned, E: DeserializeOwned + Debug, N: DeserializeOwned,
-F: FnMut(N)
-{
-    for res in reader.lines() {
-        match res {
-            Err(_) => (),
-            Ok(line) => {
-                let regex = Regex::new(r"^[0-9]+$").unwrap();
-                if regex.is_match(&line) {
-
-                } else {
-                    match decode_async::<T,E,N>(&line)? {
-                        AsyncAnswer::Finished(data)
-                            => return Some(data),
-                        AsyncAnswer::Failed(failed)
-                            => panic!("building session failed: {:?}", failed),
-                        AsyncAnswer::Note(val) => prog(val)
-                    }
-                }
-            }
-        }
-    };
-    None
-}
-
-fn get_async_task_id (reader: &mut BufReader<ChildStdout>) -> TaskID {
-    let mut res = String::new();
-    reader.read_line(&mut res).unwrap();
-    match decode_sync(&res).unwrap() {
-        SyncAnswer::Ok(AsyncStartOk { task }) => task,
-        SyncAnswer::Error(_) => panic!("failed to start async task!")
-    }
-}
 
 #[derive(StructOpt)]
 #[structopt(name = "isabelle-proto-POC", about="proof of concept for communicating with an Isabelle server")]
diff --git a/isabelle-proto/src/pipe.rs b/isabelle-proto/src/pipe.rs
new file mode 100644
index 0000000..ef80ff3
--- /dev/null
+++ b/isabelle-proto/src/pipe.rs
@@ -0,0 +1,63 @@
+
+use regex::Regex;
+use serde::Deserialize;
+use std::{io::{BufRead, BufReader}, process::ChildStdout};
+
+use crate::messages::*;
+
+pub(crate) fn decode_sync<'a, T> (msg: &'a str) -> Option<SyncAnswer<T, String>>
+where T: Deserialize<'a> {
+    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
+    let mat = regex.find(msg)?;
+    let ty = &msg[..mat.end()];
+    let rest = &msg[mat.end()..];
+
+    match ty {
+        "OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)),
+        "ERROR" => Some(SyncAnswer::Error(rest.to_owned())),
+        _ => None
+    }
+}
+
+pub(crate) fn decode_async<'a,T,E,N> (msg: &'a str) -> Option<AsyncAnswer<T,E,N>>
+where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> {
+    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
+    let mat = regex.find(msg)?;
+    let ty = &msg[..mat.end()];
+    let rest = &msg[mat.end()..];
+
+    match ty {
+        "NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)),
+        "FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)),
+        "FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)),
+        _ => None
+    }
+}
+
+
+
+
+pub(crate) fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
+    for res in pipe.lines() {
+        match res {
+            Err(_) => (),
+            Ok(line) => {
+                let hello : Option<SyncAnswer<ClientHello, _>> = decode_sync(&line);
+                if let Some(SyncAnswer::Ok(data)) = hello {
+                    return Some(data);
+                }
+            }
+        }
+    }
+    None
+}
+
+
+pub(crate) fn get_async_task_id (reader: &mut BufReader<ChildStdout>) -> TaskID {
+    let mut res = String::new();
+    reader.read_line(&mut res).unwrap();
+    match decode_sync(&res).unwrap() {
+        SyncAnswer::Ok(AsyncStartOk { task }) => task,
+        SyncAnswer::Error(_) => panic!("failed to start async task!")
+    }
+}
diff --git a/isabelle-proto/src/session.rs b/isabelle-proto/src/session.rs
index 11fb5bc..b1716d6 100644
--- a/isabelle-proto/src/session.rs
+++ b/isabelle-proto/src/session.rs
@@ -5,10 +5,7 @@ use serde::de::DeserializeOwned;
 use serde_json::Value;
 
 use crate::messages::*;
-
-use crate::{decode_async, get_async_task_id, wait_for_client};
-
-
+use crate::pipe::*;
 
 pub struct IsabelleSession {
     reader : BufReader<ChildStdout>,
@@ -121,7 +118,6 @@ impl IsabelleSession {
                 }
             }
         }
-         unreachable!{}
-        None
+        unreachable!{}
     }
 }