diff options
| author | Alasdair Armstrong | 2018-04-06 14:47:12 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2018-04-06 14:47:12 +0100 |
| commit | 922fec6b584a9de72c42036fbb415fa3e06a7a4e (patch) | |
| tree | a09c4c9411e7e47f48a5e14ec1850542c87eb23c | |
| parent | 650d7affe4704959d177579957bef749c5499158 (diff) | |
Update sail.tex for wip latex output
Fix a bug in initial check which caused X() = y to expect an additional parameter.
Some tweaks to sail2 emacs mode
| -rw-r--r-- | editors/sail2-mode.el | 2 | ||||
| -rw-r--r-- | lib/sail.tex | 9 | ||||
| -rw-r--r-- | src/initial_check.ml | 2 |
3 files changed, 10 insertions, 3 deletions
diff --git a/editors/sail2-mode.el b/editors/sail2-mode.el index 60cd762e..76024830 100644 --- a/editors/sail2-mode.el +++ b/editors/sail2-mode.el @@ -30,6 +30,8 @@ ("~" . font-lock-negation-char-face) ("\'[a-zA-Z0-9_]+" . font-lock-variable-name-face) ("\\([a-zA-Z0-9_]+\\)(" 1 font-lock-function-name-face) + ("function \\([a-zA-Z0-9_]+\\)" 1 font-lock-function-name-face) + ("val \\([a-zA-Z0-9_]+\\)" 1 font-lock-function-name-face) ("\\_<\\([0-9]+\\|0b[0-9_]+\\|0x[0-9a-fA-F_]+\\|true\\|false\\|bitone\\|bitzero\\)\\_>\\|()" . font-lock-constant-face))) (defconst sail2-mode-syntax-table diff --git a/lib/sail.tex b/lib/sail.tex index a1ae86c0..d6c6d894 100644 --- a/lib/sail.tex +++ b/lib/sail.tex @@ -3,7 +3,9 @@ \usepackage[svgnames]{xcolor} \usepackage{fullpage} \usepackage{listings} -\usepackage[hidelinks]{hyperref} +\usepackage{hyperref} + +\hypersetup{colorlinks=true,linkcolor=DarkRed} \lstset{ basicstyle=\ttfamily\small, @@ -13,7 +15,7 @@ } \lstdefinelanguage{sail} - { morekeywords={val,function,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof + { morekeywords={val,function,cast,type,forall,overload,operator,enum,union,undefined,exit,and,assert,sizeof, scattered,register,inc,dec,if,then,else,effect,let,as,@,in,end,Type,Int,Order,match,clause,struct}, keywordstyle={\bf\ttfamily\color{blue}}, morestring=[b]", @@ -30,6 +32,9 @@ \lstset{language=sail} +\def\sail{\trivlist \item\relax} +\def\endsail{\endtrivlist} + \begin{document} \include{out} diff --git a/src/initial_check.ml b/src/initial_check.ml index 12d56484..22e8bb16 100644 --- a/src/initial_check.ml +++ b/src/initial_check.ml @@ -555,7 +555,7 @@ and to_ast_lexp (k_env : kind Envmap.t) (def_ord : order) (Parse_ast.E_aux(exp,l (match f with | Parse_ast.Id(id) -> (match List.map (to_ast_exp k_env def_ord) args with - | [] -> LEXP_memory(to_ast_id f',[]) + | [E_aux(E_lit (L_aux (L_unit, _)), _)] -> LEXP_memory(to_ast_id f',[]) | [E_aux(E_tuple exps,_)] -> LEXP_memory(to_ast_id f',exps) | args -> LEXP_memory(to_ast_id f', args)) | _ -> typ_error l' "memory call on lefthand side of assignment must begin with an id" None None None) |