# HG changeset patch # User wenzelm # Date 1521150215 -3600 # Node ID 599753dd6501e7fa730ce117a8b5b793debebd54 # Parent e4e740ba74a479f253f288b689a6fb6b518427bf more comments; diff -r e4e740ba74a4 -r 599753dd6501 src/Pure/General/json.scala --- a/src/Pure/General/json.scala Thu Mar 15 22:41:59 2018 +0100 +++ b/src/Pure/General/json.scala Thu Mar 15 22:43:35 2018 +0100 @@ -2,6 +2,8 @@ Author: Makarius Support for JSON: https://www.json.org/. + +See also http://seriot.ch/parsing_json.php "Parsing JSON is a Minefield". */ package isabelle