adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

autolevity: make output more JSON compliant

This commit is contained in:
Daniel Matichuk 2016-05-17 15:33:38 +10:00 committed by Alejandro Gomez-Londono
parent 7553a4e72c
commit cd21f597c1
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
lib/AutoLevity_Theory_Report.thy
View File

@ -85,7 +85,7 @@ ML_Antiquotation.inline @{binding string_record}
fun mk_elem nm _ value =
(ML_Syntax.print_string nm ^ "^ \" : \" ") ^ "^ (" ^ value ^ ")"
(ML_Syntax.print_string (quote nm) ^ "^ \" : \" ") ^ "^ (" ^ value ^ ")"
fun mk_head body =
"(\"" ^ "{\" ^ String.concatWith \", \" (" ^ body ^ ") ^ \"}\")"
@ -425,14 +425,14 @@ fun add_commas (s :: s' :: ss) = s ^ "," :: (add_commas (s' :: ss))
fun string_reports_of (thy_nm, thy_parents, lemmas, consts, types) =
["{theory_name : " ^ quote thy_nm ^ ",",
"theory_imports : ["] @
["{\"theory_name\" : " ^ quote thy_nm ^ ",",
"\"theory_imports\" : ["] @
add_commas (map (theory_entry_encode) thy_parents) @
["],","lemmas : ["] @
["],","\"lemmas\" : ["] @
add_commas (map (lemma_entry_encode) lemmas) @
["],","consts : ["] @
["],","\"consts\" : ["] @
add_commas (map ( dep_entry_encode) consts) @
["],","types : ["] @
["],","\"types\" : ["] @
add_commas (map ( dep_entry_encode) types) @
["]}"]
|> map (fn s => s ^ "\n")